Model Checking Solutions for Assignment 10 October 9, 2017 1. Suppose the set of atomic propositions is {p1, p2}. Consider the following transition system -
s0 s1
s2
{p1} {p2}
{p1, p2}
Which of the following sets gives the (exact) set of states satisfying the formula EX(p1∧p2)? (for instance, choice (a) meanss0satisfies the formula and the other statess1, s2do not satisfy the formula)
(a) {s0} (b) {s1} (c) {s2} (d) {s0, s1}
(e) {s0, s1, s2}
Solution: (d) s2 is the only state where (p1∧p2) is true. s0 and s1 are the predecessors of s2, hence the formula is true on only these two states.
2. Consider the transition system in the previous question, which of the following sets gives the (exact) set of states satisfying the formula EX EX(p1∧p2)?
(a) {s0} (b) {s1} (c) {s2} (d) {s0, s1}
(e) {s0, s1, s2}
Solution: (e)EX(p1∧p2) is true ons0ands1. And from all the states it is possible to reach eithers0
ors1 in one step. Hence, the given formula is true in all of the states of the transition system.
3. Suppose the set of atomic propositions is {p1, p2}. Consider the following transition system -
s0
s1
s3
s2
{p1} {p2}
{p1, p2} {}
Which of the following sets gives the (exact) set of states satisfying the formula E(p1U p2)?
Model Checking Assignment 10, Page 2 of 3 October 9, 2017 (a) {s1, s3}
(b) {s0, s2} (c) {s0, s3} (d) {s0, s2, s3}
Solution: (d)p2 is true ins2 and s3. So the formula is true in these two states. p1 is true in s0, and this state is a predecessor ofs2, so the formula is also true in this state. In the states1, the proposition p1 is false, hence, the formula is also false in this state.
4. Consider the transition system in the previous question, which of the following sets gives the (exact) set of states satisfying the formula E(p1 U (¬p1∧p2))?
(a) {s1, s3} (b) {s0, s2} (c) {s0, s3} (d) {s0, s2, s3}
Solution: (d) (¬p1∧p2) is true ins3. p1 is true in s0 and s2. s2 satisfies the given formula sinces2 is a predecessor ofs3. s0 also satisfies the formula because of the path s0 →s2 →s3. Check that the formula is true in no other state.
5. Suppose the set of atomic propositions is {p1, p2}. Consider the following transition system -
s0
s1
s3
s2
{p1} {p2}
{p1, p2} {}
Which of the following sets gives the (exact) set of states satisfying the formula EG p1? (a) {s0, s1, s2, s3}
(b) {s0, s2, s3} (c) {s3, s2} (d) {s0, s2}
Solution: (d) After marking all the states withEG p1, we can remove the statess1ands3, sincep1 is not true on these states. Since, there is the paths0→s2→s0, the formula is true on the two statess0
ands2.
6. Consider the transition system in the previous question, which of the following sets gives the (exact) set of states satisfying the formula EG EXp1?
(a) {s0, s1, s2, s3} (b) {s0, s2, s3}
Model Checking Assignment 10, Page 3 of 3 October 9, 2017 (c) {s3, s2}
(d) {s0, s2}
Solution: (a) SinceXp1 is true on all the states, so is the given formula.
