Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
cs-486:homework-7 [2017/02/21 18:00]
egm [Problems]
cs-486:homework-7 [2018/11/02 22:21] (current)
egm [Problems]
Line 5: Line 5:
 == Problems == == Problems ==
  
-'''​(12 points)'''​ For the transition system, which states satisfy the formulas. L(s1) = {a}. L(s2) = {a}. L(s3) = {a,b}. L(s4) = {b}. s1 -> s2. s2 -> s3. s3 -> s1. s4 -> s2. s3 and s4 are initial states. ​  +'''​1. (12 points)'''​ For the transition system, which states satisfy the formulas. L(s1) = {a}. L(s2) = {a}. L(s3) = {a,b}. L(s4) = {b}. s1 -> s2. s2 -> s3. s3 -> s1. s4 -> s2. s3 and s4 are initial states. ​  
-## X a +* A(X a) 
-## XXX a +* A(XXX a) 
-## [] b +* A([] b) 
-## []<>​a +* A([]<>a) 
-## [](b U a) +* A([](b U a)
-## <>(b U a) +* A(<>(b U a)
-# '''​(12 points)'''​ This problem is Exercise 5.5 in [http://​is.ifmo.ru/​books/​_principles_of_model_checking.pdf Principles of Model Checking ] (page 321 of the PDF document), ​consider ​an elevator system that services N > 0 floors numbered 0 through N-1. There is an elevator door at each floor with a call-button and an indicator light that signals whether or not the elevator has been called. For simplicity, consider N=4. Present a set of atomic propositions-try to minimize that set-that are needed to describe the following properties of the elevator ​as LTL formulae and give the LTL formulae: +Hint: consider each state as the starting state for the formula.
-## Any door on any floor is never open when the elevator is not present +
-## A requested floor will be served eventually +
-## The elevator repeatedly returns to floor 0 +
-## When the top floor is requested, the elevator serves it immediately and does not stop on any floor on the way up+
  
-'''​1.'''​ ('''​points'''​) For each of the following properties: label as either safety or liveness, express in a CTL* formula, and create a minimal label trace to satisfy written formula.+'''​2. (16 points)'''​ This problem is Exercise 5.5 in [http://​is.ifmo.ru/​books/​_principles_of_model_checking.pdf Principles of Model Checking ] (page 321 of the PDF document), consider an elevator system that services N > 0 floors numbered 0 through N-1. There is an elevator door at each floor with a call-button and an indicator light that signals whether or not the elevator has been called. For simplicity, consider N=4. Present a set of atomic propositions-try to minimize that set-that are needed to describe the following properties of the elevator as LTL formulae and give the LTL formulae: 
 +* Any door on any floor is never open when the elevator is not present 
 +* A requested floor will be served eventually 
 +* The elevator repeatedly returns to floor 0 
 +* When the top floor is requested, the elevator serves it immediately and does not stop on any floor on the way up 
 + 
 +'''​3.'''​ ('''​16 points'''​) For each of the following properties: label as either safety or liveness, express in a CTL* formula, and create a minimal label trace to satisfy written formula.
    
 * The number of items in a buffer may not exceed ''​n''​ * The number of items in a buffer may not exceed ''​n''​
Line 25: Line 27:
 * It is always cloudy before it rains * It is always cloudy before it rains
  
-'''​2.'''​ ('''​points'''​) Express the following property in LTL (the '​!'​ operator is a logical not):+'''​4.'''​ ('''​points'''​) Express the following property in LTL (the '​!'​ operator is a logical not):
  
 ''​the transition from !p to p will happen at most once''​ ''​the transition from !p to p will happen at most once''​
  
-'''​3.'''​ ('''​points'''​) Express the following property in LTL:+'''​5.'''​ ('''​points'''​) Express the following property in LTL:
  
 ''​there are infinitely many transitions from !p to p (and vice versa)''​ ''​there are infinitely many transitions from !p to p (and vice versa)''​
  
-'''​4.'''​ ('''​points'''​) Express the following property in LTL using ''​r'',​ ''​y'',​ ''​g''​ as atomic propositions denoting the states of the traffic light (r = red, y = yellow, g = green):+'''​6.'''​ ('''​points'''​) Express the following property in LTL using ''​r'',​ ''​y'',​ ''​g''​ as atomic propositions denoting the states of the traffic light (r = red, y = yellow, g = green):
  
 ''​The lights of a traffic signal light in the following periodic sequence: red, yellow, green, red, yellow, green,... and only one light is on at any given time, starting with red. You cannot make any assumptions on how long a light is on other than it will be on for a finite length of time.''​ ''​The lights of a traffic signal light in the following periodic sequence: red, yellow, green, red, yellow, green,... and only one light is on at any given time, starting with red. You cannot make any assumptions on how long a light is on other than it will be on for a finite length of time.''​
  
-'''​5.'''​ ('''​points'''​) Express the following property in LTL:+'''​7.'''​ ('''​points'''​) Express the following property in LTL:
  
 ''​if q holds in a state si and r holds in some subsequent state (sj , j > i) then p must not hold in any state sk in between si and sj (i < k < j , where j is the first such subsequent state)''​ ''​if q holds in a state si and r holds in some subsequent state (sj , j > i) then p must not hold in any state sk in between si and sj (i < k < j , where j is the first such subsequent state)''​
  
  
cs-486/homework-7.1487700035.txt.gz · Last modified: 2017/02/21 18:00 by egm
Back to top
CC Attribution-Share Alike 4.0 International
chimeric.de = chi`s home Valid CSS Driven by DokuWiki do yourself a favour and use a real browser - get firefox!! Recent changes RSS feed Valid XHTML 1.0