1. (20 points) Which equivalences are true (justify your answer with a proof or counter-example)

• []f → <>g ⇔ f U (g \/ !f)
• X <> f1 ⇔ <> X f1
• (f U g) U g ⇔ f U g
• [] f /\ X <> f ⇔ []f
• <> f /\ X []f ⇔ <>f

2. (20 points) The CTL formula AF (AG p) is stronger than the LTL formula FG p meaning that a particular Kripke structure may model FG p but not AF (AG p). Draw such a Kripke structure and explain why that Kripke structure does not satisfy the CTL formula. Also prove that if a system satisfies the CTL formula, it must also satisfy the LTL formula. In what situation might you want to use the stronger formula (finding bugs or verifying correctness)? Hint: there are only three states in the Kripke structure.

3. (25 points) The LTL formula GF p is stronger than the CTL formula AG (EF p) meaning a Kripke structure may model AG (EF p) but not model GF p. Draw such a Kripke structure and explain why that Kripke structure does not satisfy the LTL formula. Also prove that if a system satisfies the LTL formula, it must also satisfy the CTL formula. Hint: there are only two states in the Kripke structure.

4. (20 points) Explain why the CTL* formula E(GF p) is not equivalent to either of the CTL formulas EG(EF p) and EG(AF p). For each pair of (CTL*, CTL) formula, state which property is stronger, and draw a Kripke structure that satisfies the weaker property but not the stronger property.

5. (10 points) Is [(EF p) || (EF q)] equivalent to EF(p || q) where the '||' operator is logical OR? Justify your answer.

6. (10 points) Is [(AF p) || (AF q)] equivalent to AF(p || q)? Justify your answer.