A(phi) holds on every state that has no infinite path. Please explain this

Question

I have a problem  from 2017 Feb Que 4     ---  S4=A[bUc]

My understanding is on ALL the INFINITE paths b holds until c or only b holds. But A(phi) holds on every state that has no infinite path contradicts this. Can you please explain when is  A(phi) and E(phi)  holds ? And how does s7 ,s8 and s3 holds for this?

Comments

All infinite paths also means that we are immediately happy if a state has no infinite paths. That's why s8 is said to satisfy the formula.

A state with c satisfies the formula as well as the path until “ends“ there. That's why s3 and s7 are satisfying. The states s6 and s1 are not satisfying as they do have edges leading to states not satisfying b. That means not all of their paths satisfy the until criterion. That's why s1 and s6 are not satisfying.

Answer 1

We are talking about this state transition system:

States s3,s7,s8 are states labeled with c. Thus, all infinite paths leaving these states satisfy [b WU c] and even the strong until [b SU c] (even if b would be false) since c is initially true on these paths. Now, s8 does not have infinite outgoing paths while s3 and s7 have these. This does however not matter for A quantifiers, since their meaning is: "If there are infinite outgoing paths, then all of them have to satisfy the path property. If there is no infinite outgoing path, then ALL formulas AΦ are true in that state."

Hence, any formula  AΦ would hold in state s8 (so it is not needed that c was on the label). Saying "any" is really meant this way, since even A false holds in state s8 (as in any other state without outgoing infinite path).

Comments

Since it  is weak until A[bUc], shouldn't we check for b rather than on c?? c might or might not occur. So this is equal to AG(b) if c does not occur. If this is the case, ten S6,s1 and s8 holds.

---

sorry got it. Thank you

---

Maybe another note could be helpful: E[b SU c] holds in states s3,s6,s7. In s7 because there in an infinite path and in the initial state of that one (which is s7), c holds and therefore also E[b SU c] holds. The same is the case for s3, and for s6 we really have first b and then on the way to s3 also c (and what follows does not matter unless it can be continued for infinitely many transitions). s8 is not on the list, since s8 does not have an infinite path. s6 does not hold for A[b SU c] since other paths leaving s6 do not satisfy [b SU c].