Description
- Show φ U ψ ≡ ψ R (φ ∨ ψ) ∧ Fψ using semantic equivalences.
- Give a model M = (S,→,L) and s ∈ S such that M,s |= AF(φ ∨ ψ) but M,s 6|= AFφ ∨ AFψ.
- Express the following statement in CTL∗:
“the event p is never true between the events q and r on a path.”
- Show AGFp and AGEFp specify different properties.
