generated at
2/17/2025, 5:16:08 PM
時相演算子
temporal operator
\mathbf{X}
neXt
経路上の次の状態で
\bigcirc
と書くこともある
\mathbf{G}
Globally
経路上の任意の状態で
\Box
と書くこともある
\mathbf{F}
Finally
経路上のある状態で
なぜ「Finally?」
\Diamond
と書くこともある
\mathbf{U}
Until
AUBは、Bが成り立つまでAが成り立つ
