##### Differences

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

 cs-486:homework-7 [2017/02/21 11:05]egm [Problems] cs-486:homework-7 [2018/11/02 16:21]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 Line 6: Line 6: '''​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.  ​ '''​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)) + Hint: consider each state as the starting state for the 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: '''​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: