1. (16 points) Draw the expression tree for the following CTL formula: $\mathrm{EX}\ a \wedge \mathrm{E}(b\ \mathrm{U}\ \mathrm{EG}\ \neg c)$

2. (10 points) Write the equivalent formula for the one presented that only uses EX, EU, and EG for path-temporal operators: $\mathrm{AG}(a \rightarrow \mathrm{AF}(b \wedge \neg a))$. Show any intermediary steps.

3. (10 points) Write the equivalent formula for the one presented that only uses EX, EU, and EG for path-temporal operators: $\mathrm{AX}(\mathrm{E}(\neg a\ \mathrm{U}\ (b \wedge c)) \vee \mathrm{EG}\ \mathrm{AX}\ a)$. Show any intermediary steps.

4. (36 points) Do Exercise 6.1 in Principles of Model Checking (page 452 of the PDF document). Convert any formula to existential normal form as needed.

5. (8 points) For the tree in problem one, replace any sub-formulas with equivalent least or greatest fix point computations.

6. (6 points) Consider the formula $\mathrm{EG} f$. Draw a transition system for which it takes 4 iterations on the equivalent fix-point calculation to reach the fix-point. Show the labeled set of state on each iteration.

7. (6 points) Consider the formula $\mathrm{EF} f$. Draw a transition system for which it takes 5 iterations on the equivalent fix-point calculation to reach the fix-point. Show the labeled set of states on each iteration.