Model Checking Solutions for Assignment 9 October 2, 2017 1. A tree satisfies a CTL state formulaϕif there exists some node in the tree satisfyingϕ- is this statement
true or false?
(a) True (b) False
Solution: (b) A tree satisfies a state formulaϕif its root satisfies the state formulaϕ.
2. Is A(EXp U EF(¬p)) a syntactically correct CTL formula?
(a) Yes (b) No
Solution: (a) Yes
3. Is (AEXp)U (AEF(¬p)) a syntactically correct CTL formula?
(a) Yes (b) No
Solution: (b) No.
4. Is EX(¬true) a syntactically correct CTL formula?
(a) Yes (b) No Solution: (a)
5. Does there exist a transition system whose computation tree satisfies the formula given in the previous question?
(a) Yes (b) No
Solution: (b) Since¬trueis never true on any vertex.
6. Let the set of atomic propositions be{a, b, c}. Does the transition system given below satisfyA(aU b)?
DMTH Model Checking Examination January 13, 2014
NOT
AND OR
r
x y
s0 s1
{p1},{p1, p2}
{p1},{p1, p2}
{ },{p2} { },{p2}
XOR
r
x y
x= 0, r= 1, y= 1
x= 0, r= 0, y= 0
x= 1, r= 1, y= 0
x= 1, r= 0, y= 1
s0
s1
s2
s3 s4
{a}
{a, b}
{b, c} {c}
{c}
s0
s1 s2
s3
s4 {}
{b} {a, b} {a}
{b}
(a) Yes (b) No
Solution: No. The root state satisfies neitheranorb.
Model Checking Assignment 9, Page 2 of 2 October 2, 2017 7. Does the transition system given in Question 6 satisfy EX AG b?
(a) Yes (b) No
Solution: Yes. The paths0(s4)ω satisfies is a witness satisfying this formula.
8. Does the transition system given below satisfy the formulaEF AG c?
DMTH Model Checking Examination January 13, 2014
NOT
AND OR
r
x y
s0 s1
{p1},{p1, p2}
{p1},{p1, p2}
{ },{p2} { },{p2}
XOR
r
x y
x= 0, r= 1, y= 1
x= 0, r= 0, y= 0
x= 1, r= 1, y= 0
x= 1, r= 0, y= 1
s0
s1
s2
s3 s4
{a}
{a, b}
{b, c} {c}
{c}
(a) Yes (b) No
Solution: Yes. The paths0s1(s4)ωsatisfies is a witness satisfying this formula.
