Interpreting CTL formulas

Question

 S1 = E((Fb) ∧ EG¬a) 

S2 = EF(b ∧ EG¬a)

For this question i believe S1 means there is a path where E(Fb) is true and there is a path where E(EG¬a ) is true but we do not need to be in either of the paths, the path just needs to exists

S2 means there is a path where at some point in time b ∧ EG¬a must hold and that is not satisfied by either path.

Is my understanding correct ?

Answer 1

I think your understanding is correct. I just wouldn't have put the additional E-quantifiers around E(Fb) and E(EG¬a).

Look at the path from s0 to s1, looping at s1. This is a path satisfying G¬a.

This path exists from s0.

Now look at the path from s0 to s2, looping at s2. It satisfies Fb from the first state. It also satisfies EG ¬a in the first state.

Similarly for S2. In s0, s1, there is a path satisfying G¬a. s2 is the only state that satisfies b. But as it doesn't satisfy EG¬a, there is no path satisfying F(b ∧ EG¬a).

Comments

So just to clarify, in S1 we must have 2 separate paths because there is no one path that satisfies E((Fb) ∧ EG¬a) . I assume the reason we need 2 seperate paths is because of the outer E which just says a path exists and the inner E says there is also another path

---

I'd like to add something on this discussion. In the Kripke structure mentioned as the solution, aren't states s0 and s1 the same? Could someone please explain why we need to have s0 as initial state and the a self loop on s1 and why not have the self loop on s0 itself?

---

from my understanding, to satisfy formula s1 we need to satisfy 2 things, first one is we need a path where b is true at some point in time and also a path where !a is globally true, in s0 we can do both. s0-> s1 satisfies EG!a and s0->s2 satisfies Fb. If we had a self loop on s0 without s1, it would still be correct. so we would now have s0 -> s0 satisfying EG!a

---

That's exactly my concern. s0->s1 and s0->s0 should then be the same. Thanks for sharing your comment.

---

@daodubasit Do we need two separate paths to satisfy s1? We *can* use two separate paths but we don't have to. Think of a Kripke structure structure only consisting of a self-loop at an initial state satisfying b ∧ ¬a. The path we pick for the outer E is by chance the same path that also satisfies G¬a of the inner E.

@frzmohammadali Can we merge s0 with s1? daodubasit is right. We can. When I designed this solution, I added this additional state so that we only have two paths. I found it makes it easier to talk about the paths.

---

what you just described (a Kripke structure structure only consisting of a self-loop at an initial state satisfying b ∧ ¬a.), would satisfy S1 and S2

---

Yes. Correct. I meant: Just satisfying S1 is possible with just one state.