##### Differences

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

 cs-486:homework-7 [2017/02/21 11:00]egm [Problems] cs-486:homework-7 [2017/02/21 11:05]egm [Problems] Both sides previous revision Previous revision 2018/11/02 16:21 egm [Problems] 2017/02/21 11:05 egm [Problems] 2017/02/21 11:00 egm [Problems] 2017/02/21 10:59 egm 2017/02/21 10:58 egm created2017/01/11 12:12 egm removed2016/04/06 13:44 egm [Paper Pencil] 2014/09/02 10:43 egm created 2018/11/02 16:21 egm [Problems] 2017/02/21 11:05 egm [Problems] 2017/02/21 11:00 egm [Problems] 2017/02/21 10:59 egm 2017/02/21 10:58 egm created2017/01/11 12:12 egm removed2016/04/06 13:44 egm [Paper Pencil] 2014/09/02 10:43 egm created Last revision Both sides next revision 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 + * X a - ## XXX a + * XXX a - ## [] b + * [] b - ## []<>​a + * []<>​a - ## [](b U a) + * [](b U a) - ## <>(b U 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: + - ## 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.'''​ ('''​4 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 26: * It is always cloudy before it rains * It is always cloudy before it rains - '''​2.'''​ ('''​1 points'''​) Express the following property in LTL (the '​!'​ operator is a logical not): + '''​4.'''​ ('''​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.'''​ ('''​1 points'''​) Express the following property in LTL: + '''​5.'''​ ('''​4 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.'''​ ('''​3 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.'''​ ('''​8 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.'''​ ('''​3 points'''​) Express the following property in LTL: + '''​7.'''​ ('''​5 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)''​