search
Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | |||
|
cs-486:homework-7 [2017/02/21 11:05] egm [Problems] |
cs-486:homework-7 [2018/11/02 16:21] (current) egm [Problems] |
||
|---|---|---|---|
| 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: | ||
