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