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