状態遷移系の1つの経路に関する性質を記述する

\begin{aligned}\varphi &::= P \mid \neg \varphi \mid \varphi \vee \varphi \mid \mathbf{X}\varphi \mid \mathbf{A}(\varphi \mathbf{U} \varphi) \mid \mathbf{F}\varphi \mid \mathbf{G}\varphi\end{aligned}

CTLの論理式から経路限定子を除いたものになっている

時相演算子のみ使うということ