CTL
Computational Tree Logic
複数の経路や経路の間の関係を記述できる
BNF記法
$ \begin{aligned}\varphi &::= P \mid \neg \varphi \mid \varphi \vee \varphi \\&\mid \mathbf{EX}\varphi \mid \mathbf{E}(\varphi \mathbf{U} \varphi) \mid \mathbf{EF}\varphi \mid \mathbf{EG}\varphi \\&\mid \mathbf{AX}\varphi \mid \mathbf{A}(\varphi \mathbf{U} \varphi) \mid \mathbf{AF}\varphi \mid \mathbf{AG}\varphi\end{aligned}
記号が多いねmrsekut.icon