CTL* Sept 2022 Problem 8a

Question

Exam Sept 2022, Problem 8a

Question - S1 = AF(p | q)
S2 = AFp | AFq

In the solution provided, s0 is an empty initial state. s1 is state p with an infinite loop, and s2 is state q with an infinite loop. s0 has path to s1 and s2

Please correct my understanding - For S1 - AF(p|q) is always a path in the future; there is p(s0,s1) or q(s0,s2). So S1 satisfies all three states.

For S2: According to my understanding, There is always a path in the future AF(p) is satisfied in (s0,s1) and AF(q) is satisfied in (s0,s2). How is it not holding in s0?

Please help me understand the significant difference. I appreciate any help you can provide.

Pavithra

Answer 1

You are wondering about this solution:

S2 is a CTL formula so that it is easy to compute the states that satisfy S2: AFp holds exactly on s2 while AFq holds exactly on s1, hence, their disjunction holds exactly on states {s1,s2}. AFp does not hold in s0 since there is a path s0->s2->s2->... where p never holds, and for the analog reason, AFq does not hold in s0. 

The formula AF(p|q) holds in the states where all outgoing infinite paths finally reach a state where p|q holds. The formula p|q holds exactly in states {s1,s2} so that these states at least also satisfy AF(p|q). AF(p|q) also holds in s0 since all paths leaving s0 must finally reach s1 or s2, hence, states where p|q holds.