CTL Satisfiability

Question

As this cannot be checked in tool, I am asking it here. I solved it on my own and I am trying to violate S2 and satisfy S1.

S1= A(!a & FGa)

S2 =A(!a & FAGa)

For the single path s0s1(s2)^w, S2 is violated since in AFAGa,  AGa does not hold in state s0 and s1. I am wondering will this be enough to violate or will AF cause issue?

Answer 1

In your structure, AG a holds in state s2, thus AF AG a holds in all states. S2 is equivalent to !a&AFAGa, hence, it holds in states s0 and s1. Also S1 holds in s0 and s1, so that your structure does not distinguish between the two.

Comments

Yes, I get your point. AF was my concern and I knew that it was wrong but I was not sure, I now have an idea on how to solve this. Thank you very much.