計算木論理
AF φ {\displaystyle \phi } == A[1U φ {\displaystyle \phi } ] == ¬ {\displaystyle \neg } EG( ¬ {\displaystyle \neg } φ {\displaystyle \phi } )
A[ φ {\displaystyle \phi } U ψ {\displaystyle \psi } ] == ¬ {\displaystyle \neg } (E[ ¬ {\displaystyle \neg } ψ {\displaystyle \psi } U ¬ {\displaystyle \neg } ( φ {\displaystyle \phi } ∨ {\displaystyle \lor } ψ {\displaystyle \psi } )] ∨ {\displaystyle \lor } EG ¬ {\displaystyle \neg } ψ {\displaystyle \psi } )
計算木論理(CTL)は線形時相論理(LTL)と同様 CTL*(英語版) のサブセットである。CTL と LTL は共通部分もあるが等価ではない。
GF.P は LTL にはあるが CTL にはない。
AG(P → {\displaystyle \rightarrow } (EF.Q)) は CTL にはあるが LTL にはない。