命題動的論理
命題動的論理Propositional Dynamic Logic，以下PDL いくつかの表現力は失う
完全性を得る
無限の規則を持っていいならある
原子プログラム$ a,b,c,\dots
論理式及びプログラム
1. 命題変項$ p_1,p_2,\dotsおよび$ \top,\botは論理式
2. 原子プログラムはプログラム
3. 論理式$ \phi,\psiとプログラム$ \piに対し
普通の命題論理の論理式，つまり$ \phi \to \psiとか$ \phi \land \psiなどは論理式である
$ \lbrack \pi \rbrack \phi, \langle \pi \rangle \phiは論理式である
4. 論理式$ \phiとプログラム$ \pi_1,\pi_2,\piに対し
$ (\pi_1;\pi_2), (\pi_1\cup\pi_2),(\pi^*),(\phi?)はプログラムである
プログラムの直感的意味
$ \pi_1;\pi_2: $ \pi_1の後に$ \pi_2を実行
$ \pi_1 \cup \pi_2: $ \pi_1または$ \pi_2のどちらかを非決定的に選択して実行
$ \pi^*: $ \pi^*を$ 0 \leq n回実行
$ \phi?: $ \phiが真なら次のプログラムを実行（あるいは正常に終了），偽ならエラー（正常に終了しない）
論理式の直感的意味
$ \lbrack \pi \rbrack \phi: $ \piがどのような過程を通ったとしても，正常に実行終了するなら$ \phiが真
$ \langle \pi \rangle \phi: $ \phiを真とするような，$ \piの正常に実行終了する過程が存在する
例えば
$ p \to \lbrack (a;b)^* \rbrack q
$ pが成立するなら，（原子）プログラム$ a,bを交互に何回繰り返し実行しても（$ a,b,a,b,\dots）$ qが成立する．
ラベル付き状態遷移系，PDLモデル，その他の記号
組$ \lang S, \overset{a_1}{\rightsquigarrow},\overset{a_2}{\rightsquigarrow},\cdots \rang はラベル付き状態遷移系とする
$ Sは非空の状態集合
原子プログラム$ a_1, \cdotsに対して$ S上の二項関係$ \overset{a_1}{\rightsquigarrow},\overset{a_2}{\rightsquigarrow},\dots
ここで原子プログラムは有限個あるいは可算無限個とする
ラベル付き状態遷移系に付値関数$ f: \mathbf{P} \to \{\mathtt{true}, \mathtt{false}\}を追加したもの
すなわち$ \mathcal{M} = \lang S, \overset{a_1}{\rightsquigarrow}, \cdots, f\rangをPDLモデルとする
$ \mathcal{M},s \models \phi
PDLモデル$ \mathcal{M}およびその状態$ sに対して$ \phiが真である
$ s \overset{\pi}{\rightsquigarrow} t
状態$ sでプログラム$ \piを実行すると状態$ tに遷移する
意味論
$ \mathcal{M},s \models \lbrack \pi \rbrack \phi
$ s \overset{\pi}{\rightsquigarrow} tとなる任意の$ tに対して$ \mathcal{M},t \models \phi
$ \mathcal{M},s \models \langle \pi \rangle \phi
$ s \overset{\pi}{\rightsquigarrow} tで，$ \mathcal{M},t \models \phiな，ある$ tが存在する
$ s \overset{\pi_1;\pi_2}{\rightsquigarrow} t
$ s \overset{\pi_1}{\rightsquigarrow} u \overset{\pi_2}{\rightsquigarrow} tな$ uが存在
$ s \overset{\pi_1 \cup \pi_2}{\rightsquigarrow} t
$ s \overset{\pi_1}{\rightsquigarrow} tまたは$ s \overset{\pi_2}{\rightsquigarrow} t
$ s \overset{\pi^*}{\rightsquigarrow} t
$ s (\overset{\pi}{\rightsquigarrow} )^n tな$ 0 \leq nが存在
$ s \overset{\phi?}{\rightsquigarrow} t
$ s = tかつ$ \mathcal{M},s \models \phi