CTL, LTL, CTL* [02.2022 7a]

Question

Would my solution work too?

Answer 1

No, it does not work. [a WU b] is not satisfied, since b never holds, but a does also not hold always. Also, [b SB !a] does not hold since b never holds (and it should even hold before !a).

Comments

I am a bit confused, since [a WU b] & F!a is given, does it mean that it is enough if [a WU b] is satisfied in t=0? like the initial state s0?

since WU is given, it means in [a WU b], b may or may not be true but a has to be true right? so, at t=0, a is true, so it would make [a WU b] true or since it is not true in next state it will be false? How does that work?

---

[a WU b] is a path formula so we have to find a path where it holds at some position (like t=0) and where the other formula does not hold. Note that [a WU b] = b | a &X[a WU b], so that [a WU b] holds at t=0 if b holds there (which is not the case) or if a holds there (which is the case) AND [a WU b] holds at t=1 (which is not the case).