Doubt regarding Temporal Logics

Question

Hi,

How does E [a SU a ] holds only in {s0,s5}? There is a path from s3 -> s5 so why it doesn't hold in s3?

Answer 1

[ a SU a ] means that we need to see the right hand a eventually, and on the way, the left hand a needs to be satisfied in every step. As all states other than {s0, s5} do not satisfy a, they also fail satisfying [ a SU a ]. Thus only {s0, s5} satisfy [ a SU a ]

Comments

okay so we wont see path here? e.g. s3 is also eventually reaching a and in SU if we have reached /si then it would be true. s3-s5-s0-s5-s0...

---

[a SU a] is equivalent to just a. Thus, it holds on every infinite path that starts with a state labeled with a. The path  s3-s5-s0-s5-s0... you mention starts with state s3 that is labeled with c, but not with a. So [a SU a] does not hold on that path.

---

s3 does not satisfy the left hand criterion. Also is does not satisfy the right hand criterion. Thus, no path starting from s3 could satisfy [ a SU a ].