CTL model checking

Question

In this question, EGc was computed as {s1,s2,s5}, we now have to compute AF(s1,s2,s5), but we have a path s5->s4->s5->s4..... that will never reach {s1,s2,s5}. But s5 satisfies it in the solution. Can you please explain why

Answer 1

The path (s5;s4)^omega reaches states s4 and s5, so why do you say it does not reach {s1,s2,s5}? Is it since you believe that all states of {s1,s2,s5} must be reached by such a path. That is not the case. However, all paths leaving a state s would have to reach one state of {s1,s2,s5} to satisfy AFEGc. Looking at the state transition diagram above, there is no state that does not do that, since all cycles of states contain at least one state of  {s1,s2,s5}. Hence, all states satisfy AFEGc.

As an alternative explanation, consider the fixpoint definition of AFp which is μx. p ∨ x. Hence, we the set of states satisfying p are definitely included, and thus also {s1,s2,s5} must be included, which means in particular that s5 does satisfy this formula.

Comments

to understand you correctly, if we have a CTL formula AF(s1,s2,s3) or EF(s1,s2,s3), any state that satisfies at least s1 or s2 or s3 satisfies the formula ?

---

Yes, you may also understand it as follows: assume you have three states sa,sb,sc that satisfy variables a,b,c, respectively, then a|b|c is satisfied by anyone of the states sa,sb,sc. Hence, if you have a set {s1,s2,s3} then each one of s1,s2,s3 satisfies this set while s1 only satisfies {s1}.

---

okay thank you. can you also please help us clarify on this question https://q2a.cs.uni-kl.de/2135/2019-august . In the final comment we were hoping to see if there is a formula that satisfies s2 and not s1

---

I have added a comment there now.