Path Quantifiers without temporal operators

Question

When we have the case t E(ϕ ∧ ψ) the slides say we need to convert the formula ϕ of Eϕ into dnf then apply E(ϕ ∨ ψ).

For this question EGE((Fb) ∧ (Fa)) we have to convert it to CTL, i am not sure of how i can convert ((Fb) ∧ (Fa)) to dnf and then apply the formula for the case E(ϕ ∨ ψ).

Answer 1

It works like this:

    E((F b) ∧ (F a))
    = E(F(a ∧ F b) ∨ F(b ∧ F a))
    = EF(a ∧ F b) ∨ EF(b ∧ F a)
    = EF(a ∧ EF b) ∨ EF(b ∧ EF a)

 Note that  Fb ∧ Fb means that at some points of time tb and ta, we have b and a, respectively. We can make a case distinction on whether b or a occurs first.

Comments

If we had ((G b) ∧ (G a)) what would the dnf form be ?

---

In that case, we proceed differently: E((G b) ∧ (G a)) = EG(b ∧ a).

---

Typo in the note. Should be Fa ∧ Fb rather than Fb ∧ Fb.