COMPUTATIONAL LOGIC-Homework 6 solved

(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