Processing math: 100%

Thursday, February 7, 2013

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)

No comments:

Post a Comment