Clarke-Emerson Theorem

The theorem gives CTL formula an iterative interpretation of their denotational semantics. \begin{align*} [\mathbf{EG} \phi] &= \nu z. ([\phi] \cap [\mathbf{EX} z]) \\ [\mathbf{E}(\phi \mathbf{U} \psi)] &= \mu z. ([\psi] \cup ([\phi] \cap [\mathbf{EX}z])) \\ [\mathbf{EF} \phi] &= \mu z. ([\phi] \cup [\mathbf{EX} z] \end{align*}

Appendix

• $[\mathbf{EX} \phi]$ is the existential pre-image of $[\phi]$.
• $\nu z. F z$ calculates the greatest fixed point.
• $\mu z. F z$ calculates the least fixed point.
• $\mathbf{EF} \phi = \mathbf{E}(\top \mathbf{U} \phi)$