経路限定子
path quantifier
$ \mathbf{E}
現在の状態から始まる経路が存在して~
経路
を考慮した
$ \exist
的な
mrsekut.icon
$ \mathbf{A}
現在の状態から始まる任意の経路に対して~
経路
を考慮した
$ \forall
的な[m