計算木論理
時相作用素には以下のものがある:
経路作用素(Path Operators) A φ {\displaystyle \phi } - All: φ {\displaystyle \phi } は現在状態から分岐する全ての経路で真である。 E φ {\displaystyle \phi } - Exists: 現在状態から分岐する経路のうち少なくとも1つの経路で φ {\displaystyle \phi } が真である。
状態作用素(State Operators) N φ {\displaystyle \phi } - Next: φ {\displaystyle \phi } は次の状態で真である(X と表記されることもある)。 G φ {\displaystyle \phi } - Globally: φ {\displaystyle \phi } はその後の全ての経路で常に真である。 F φ {\displaystyle \phi } - Finally: φ {\displaystyle \phi } はその後の経路のいずれかの時点で真となる。