Query regarding Eventual Operator

Question

Hi,

When we add Eventual operator to a path quantifier what does that generally mean? does that mean that on one path (E) or all the paths (A) phi can hold at any point of time? If yes then in the image below why does A F (a & c) holds only in s8 ? From s0 there is a path s0->s2->s8 so why are we not considering s0? 

  

Answer 1

A formula starting with “A” means: Look at all (infinite) paths from this state and check whether they satisfy the inner criterion.

Look at (s0,s2)^omega. No state on this path satisfies a&b. Thus, F(a&b) is not satisfied from its first step. Therefore, it is a counterexample to A F (a&b).

Furthermore, the path s0→s2→s8 cannot be continued to an infinite path. Thus, this wouldn't be a path for satisfying E F (a&b)

Comments

Thanks, what if there was an edge between s8 and s2? Then it would have made an infinete path between (s0s2s8)^omega. Then we would consider s0 as well?

---

For the existential quantifier, yes. We could then form an infinite path going through s8. s8 satisfies a&c. Thus, the infinite path from s0 satisfies F (a&c). Hence, the state s0 satisfies E F (a&c). But it does not satisfy A F (a&c) because we still have infinite paths (the one between s0 and s2 for example) that do not satisfy F (a&c).

---

Got it thanks, so for every property with Path Quantifier we must always look for inifinete paths!

---

If you have a quantifier like A phi, you need to check whether all infinite paths satisfy phi. If there are only finite paths, it is trivially satisfied.
If your quantifier is E phi, then there needs to be one infinite path that satisfies phi.