LTL
線形時相論理_
Linear temporal logic
状態遷移系の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
の論理式から
経路限定子
を除いたものになっている
時相演算子
のみ使うということ
/mrsekut-book-4007305803/130 ((b) 線形時間時相論理)
https://ja.wikipedia.org/wiki/線形時相論理
https://en.wikipedia.org/wiki/Linear_temporal_logic