Description

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