CTL, LTL and CTL∗

Question

Hello,

I wanted to ask in the below solution, why s1 is not satisfied?. For WU even if phi alone is satisfied, the formula would satisfy and "a" is being satisfied at initial state itself.
 

Thanks!.

Answer 1

in s0, a and thus also Fa are satisfied. From s1 on, we never see a again. Hence, Fa is not satisfied in s1. The weak until is satisfied if either the left side holds forever or at least to the point before the point when the right side is satisfied. Since b is nowhere satisfied, we'd have the left side forever but it is only satisfied in the first step. Thus, S1 isn't satisfied.

Comments

Thank You. So, for SU, formula will be satisfied even if once also the right side becomes true but doesn't have to necessarily hold forever? But for WU, the left side has to hold forever irrespective of, if its 'a' or 'Fa' (in the above case) or till the point when the right side becomes true. Have I understood it correctly?.

---

Both for SU and WU, the formula is satisfied once the right side is (provided that the left side had been satisfied so far). The difference is that WU also additionally allows the right side to never be satisfied if the left side is always satisfied.


Edit (one year later): I've been asked what's the intuition about SB and WB.
Both are satisfied if the left hand side is satisfied at some point and the right hand side has so far not been satisfied up (and including) that step.
If neither side is ever satisfied, then WB is satisfied, SB is not.