線形時相論理
普通の論理に時間の流れを付け加えたような論理
「(時刻によらず) 常に$ Pが成り立つ」「いつか必ず$ Qが成り立つ」といったステートメントを表現できる
時相論理にはいくつか種類があるが、線形時相論理は状態の列を使ってモデル化しているのが特徴。一方、計算木時相論理は状態のツリーを使う。 記号
命題論理の記号に加えて、以下ような記号が使える（他にもある） $ \square : 常に……が成り立つ
$ ◇: いつか必ず……が成り立つ
例
$ \square P: 常に$ Pが成り立つ
$ P \land \square Q : 初期状態で$ Pが成り立ち、かつ常に$ Qが成り立つ
単に$ Pと書くと初期状態で$ Pが成り立つという意味になる
$ ◇\square P: どこかの時点で$ Pが成り立ち、その後ずっと$ Pが成り立ち続ける
「$ Pが常に成り立つ」がいつか必ず成り立つ
$ \square ◇ P: $ Pが無限回発生する
「$ Pがいつか成り立つ」が常に成り立っている
$ \square (P \to ◇Q): どこかの時点で$ Pが成り立ったならば、その後必ずいつか$ Qが成り立つ
LTL の世界観
時間は離散的である
$ t = 0, 1, 2, \ldots のような感じ
時刻を決めると、そのときの状態が決まる
例: 交通信号機は、赤・黄・青の3つの状態を取る。
状態を決めると、原子命題の真偽が決まる
要するに、時間とともに状態が遷移していき、それに伴って原子命題の真偽も変わっていくような世界を考えている
パス
状態の無限長の列をパスと呼ぶ
無限長であることに注意
グラフ理論のパスは同じ頂点を2度含んではいけないが、ここでのパスにはそういう制約はない
$ \piをパスとするとき、その$ i番目の要素を$ \pi_iと書く。
$ \piをパスとするとき、その$ i番目のサフィックスを $ \pi^{(i)}と書く。
つまり $ \pi^{(i)} = [ \pi_i, \pi_{i+1}, \pi_{i+2}, \ldots ]
パス$ \piを決めると、論理式の真偽が定まる
$ \pi の下での論理式$ \phi の値を$ \pi \models \phi と書く
nojima.icon 状態遷移に制約が入っている流派もあるみたいだが、TLA+では任意の状態遷移が許されてそう
nojima.icon 状態遷移に制約を入れなくても、不正な遷移は論理式で FALSE にしてしまえばよいので TLA+ 的には任意でよいってことなのかな
LTLの論理式の意味
$ \phi がLTL固有の記号を含まないとき
$ \pi \models \phi ⇔ 状態$ \pi_0 における命題論理$ \phiの値
$ \pi \models \square \phi ⇔ 任意の非負整数$ k について$ \pi^{(k)} \models \phi が成り立つ
$ \pi \models ◇\phi ⇔ ある非負整数$ k について$ \pi^{(k)} \models \phi が成り立つ
任意のパス$ \piについて$ \pi \models \phiが成り立つとき、単に$ \phiと書く
nojima.icon ほんまか？ 単に TLA+ の慣習なだけかもしれない。