LTL,CTL & CTL*

Question

I have satisfied S2 in this question. Is it correct?

The sample solution satisfies S1.

Answer 1

No that does not really make sense to me, maybe I got something wrong. First of all, it is not the case that [a WU b] is equivalent to (F b) | (G a), why do you think so?

I am also not sure whether you are drawing one or two structures since there are two states with label s0.

The path with the self-loop on the second state s0 satisfies G(a&b) and therefore also [a WU b], but it does not satisfy F!a. However, it does also not satisfy [b SB !a] since b does not hold before a, but at the same time.

The other path starting in the left state s0 satisfies [a WU b] since b immediately holds, and it also satisfies F!a since in s1, !a holds. Hence, it satisfies S1. It does not satisfy S2 so it is opposite to what you wrote.

Comments

The path with the self-loop on the second state s0 does not satisfy F!a so it does not satisfy S1 but it does satisfy S2 i guess since b holds before !a, as b and hold at the same time. Am i wrong?

i get that my first structure is wrong.

---

Yes, you are right, I have erroneously read [b B a] instead of [b B !a].