CTL*: Conjunction between Path and State formula

Question

I was trying to understand how the statement "E((Fb)∧EGa)" satisfy given the Kripke structure(From paper 2018-Aug, question 8.e). If I understood right, "Fb" is a path formula and "EGa" is a state formula and "Fb" satisfied by infinite path on s2 and "EGa" satisfied by states s1 and s0.
How to do a conjunction between states and paths? Could you please explain how should I interpret the "E((Fb)∧EGa)" with Kripke attached below?

 
Thanks in advance.

Answer 1

You are right that EG a is a state formula that is satisfied on s₀, and s₁. Let's name this property containing  s₀, and s₁ just 'c'.

The outer quantifier E requires a path that satisfies Fb, i.e. this path shall contain a state satisfying b after finitely many steps, and satisfies the state formula that we called 'c'. When does a path formula satisfy a state formula? It does so, if the first state satisfies this state formula.

Hence, we are looking for infinite paths that reach s₂ after finitely many steps, and that starts with s₁ or s₀. The only part satisfying this property is s₀ → s₂ → s₂ → …

Now we evaluate the quantifier E. It tells us the states that have a path that is one of the previously determined paths. As there is only one path of this kind, its first state s₀ is determined by the outer E.

Answer 2

In essence, state formulas express properties of states, and path formulas express properties of paths. However, the two sets of formulas are recursively defined and are mutually dependent (every state formula is also a path formula). Thus, also the semantics of the two sets of formulas is connected. The point that you missed is that every state formula is also a path formula, and its meaning on a path pi at a point of time t is as follows: K,(K,π,t) |= φ iff (K,π(t)) |= φ. This technical definition is also required to define the semantics of atomic path properties, i.e., variables.

Considering the mentioned example, we first consider EGa which holds in states {s0,s1} since these states have an outgoing infinite path where always a holds, and since s2 has only one outgoing path that does only loop on s2 and does not satisfy Ga. Having seen that, you may now abbreviate z := EGa and label the structure such that exactly states {s0,s1} are labeled with z. The given formula E((Fb)∧EGa) becomes E((Fb)∧z) so that we have to check for each state whether there is an outgoing infinite path such that (Fb)∧z holds on it at position 0. Now, let's check the three states:

• State s1 has only one outgoing path where never b holds, so it does not satisfy the formula E((Fb)∧z). 
• State s2 has only one outgoing path where always b holds, thus also Fb holds, but initially z does not hold on that path. So, s2 does also not satisfy E((Fb)∧z). 
• State s0 does satisfy the formula, since the path s0,s2,s2,... satisfies Fb and initially, we have z on that path, i.e., on s0 the variable z holds.

It is therefore easiest to understand this connection if you just abbreviate subformulas that are state formulas as new variables. Variables are also state formulas, and are evaluated on a path π at position t just by looking whether state π(t) is labeled with that variable. Without abbreviations, you just have to check whether the state π(t) satisfies the state formula.

Comments

Thanks for the clarification on the fact every state formula is also a path formula.

"States s2 has also one outgoing path where never b holds, but initially z does not hold on that path."
- Little confused, isn't s2 has an infinite path satisfying b?

"Finally, state s1 does satisfy the formula, since the path s0,s2,s2,... satisfies Fb and initially, we have z on that path, i.e., on s0 the variable z holds."
- Doesn't s0 satisfy the formula?

---

You were right, there were some typos in the answer text that I have now correct.

---

Thanks for the clarification.