A and E path quantifiers

Question

When we say there is a state whose path statisfies a condition e.g. A(c) does it mean the current state and all paths from that state must also satisfy c. E.g. in the picture above, the states whose paths satisfy A(c) are s0 and s2 because s0 is a deadend and s2 satisfies c and it's path also satisfies c.

For E(c) does it equally mean the states which have at least one path that satisfies c. E.g. in the picture above only s2 satisfy E(c)

Answer 1

A(p) holds in a state iff all infinite paths leaving that state satisfy p.  Typically, p is not a state formula, but a path formula, since otherwise, A(p) would just mean that (E true) → p, i.e., if there are infinite outgoing paths, then p must hold in the current state. Since all infinite paths leaving the current state share the same initial state (which is the current state), this implies that the current state must satisfy p.

In your structure A(c) holds in s0 and s2, as you say, but also in s5.

E(p) holds in a state iff there is at least one infinite paths leaving that state that satisfies p. Again, if p should be a state formula, then it would mean (E true)∧p, i.e., there should be an infinite outgoing path, and the current state must satisfy p.

You may also recall E(p) = ¬¬E(p) = ¬A(¬p).

Comments

why does A(c) hold in s5 since s5 has 2 other outgoing paths that are infinite and those paths do not satisfy c

---

i think i worded my question a bit wrongly and this is causing further confusion. i have reworded it, but i am still not sure if you mean that A(p) is satisfied when all infinite paths in a state satisfy c and when the initial state also satisfies c

---

Just to avoid confusion: With c you mean the variable c that appears on the states of the Kripke structure, right? If so, then A(c) is equivalent to (E true) -> c, i.e., (A false) | c which means that the state is either a deadens state or c holds there. Therefore, A(c) holds on states {s0;s2;s5}. s0 is a deadend state, and states s2 and s5 are labelled with c.

You may use the model checker https://es.cs.uni-kl.de/tools/teaching/ModelChecking.html with the following input

    vars a,b,c;
    init 2,4;
    labels 0:; 1:a; 2:a,c; 3:a,b; 4:b; 5:c;
    transitions 1->2; 1->3; 2->5; 3->0; 3->5; 4->5; 5->1; 5->4;
    specification: (nu x. <>x) -> c

Note that nu x. <>x describes exactly the states that have an outgoing infinite path, i.e., E true.

If p would be a path formula, then A(p) means that on all outgoing infinite paths, the path formula p must hold. If there are no outgoing infinite paths, then it is trivially true.

---

thanks for clarifying i understand that now, i have one more question.
To give a better overview before i ask my question, the problem is to compute the set of states that
satisfy EX(E [b SU a] ∨ A [c U c]) in the kripke structure above.

A[c u c] = A(c), now we also have to find the set of states that satisfy E [b SU a]

 E [b SU a] means there is at least an infinite path where b is true until a becomes true or
a is always true

My doubt lies in what is considered a path, from my understanding a path refers to the outgoing nodes
of a state. The states which have paths that satisfy  E [b SU a] are {s1,s2,s3}. s2 has only one path to
s5 which does not satisfy E [b SU a] but the initial state i.e. s2 satisfies E [b SU a].

My question is then if initial states are considered as paths too.

---

I see that you are confusing states, paths and transitions.

A transition is connecting just two states like s2->s5, but that is not yet a path. A path is an infinite sequence of such transitions. Looking at s2, we have the following paths:

    s2 -> s5 -> s4 -> s5 -> ...
    s2 -> s5 -> s1 -> s3 -> s5 -> ...

Anyone of these states satisfies E[b SU a] since s2 already satisfies a. The same holds for s1 and s3 which are the remaining two states that satisfy E[b SU a].

Initial states are states, and not transitions. But with the model checking algorithm, we compute the set of states that satisfy a formula, for instance, we get 〖EX(E[b SU a] | A[c SU c]))〗= {s1;s2;s3;s4;s5}, and then, we need to check whether ALL initial states are contained in that set of states. Your structure has initial states s2 and s4, so the formula holds on the structure.

---

thanks for the clarification, got it now