Objectives

- Turn CTL formulas into expression trees
- Convert CTL formulas into equivalent formulas with only EX, EU, and EG for path-temporal operators
- Build label sets given a transition system and CTL formula
- Show how to use least and greatest fix-points to do CTL model checking

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