時相演算子
temporal operator
$ \mathbf{X}
neXt
経路上の次の状態で
$ \bigcirc
と書くこともある
$ \mathbf{G}
Globally
経路上の任意の状態で
$ \Box
と書くこともある
$ \mathbf{F}
Finally
経路上のある状態で
なぜ「Finally?」
mrsekut.icon
$ \Diamond
と書くこともある
$ \mathbf{U}
Until
AUBは、Bが成り立つまでAが成り立つ