[SOLVED] COMPUTATIONAL-LOGIC Homework 6

• 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.