計算木論理
φ {\displaystyle \phi } U ψ {\displaystyle \psi } - Until: φ {\displaystyle \phi } は、ある時点で ψ {\displaystyle \psi } が真となるまでは真である。これは、将来 ψ {\displaystyle \psi } が真かどうか検証されることを意味する。 φ {\displaystyle \phi } W ψ {\displaystyle \psi } - Weak until: φ {\displaystyle \phi } は、 ψ {\displaystyle \psi } が真となるまでは真である。U との違いは、将来 ψ {\displaystyle \psi } が真かどうか検証される保証がない点である。"unless"" 作用素とも呼ぶ。
CTL* では、時相作用素は自由に混合できる。CTL では作用素は上記のように2つにグループ分けされ、経路作用素と状態作用素の組み合わせだけが可能である。後述の例を参照されたい。