Propositional Dynamic Logic of Looping and Converse
Propositional Dynamic Logic of Looping and Converse
注意 : 本記事は記事の体をなさぬ自分用メモです。したがってわかりやすさ等について一切の配慮をしておりません。内容を整理し記事の体をなすようになれば「記事の体をなさぬメモ」タグを外します。
Intro
fact
- すべての充足可能な式は有限生成可能なモデルをもつ(モデルは有限グラフのunravelingによって得られる)
- ⇧のことがPDL with loopingが有限モデル性を失わない理由.
有限モデル性
- PDL式pの(無限かもしれない)任意のモデルは,全く同じpの部分式を満たすような状態を一つにまとめる事で, pの小さな有限モデルへ縮小することができる
- PDLの決定手続きにおいて重要な性質(Fischer and Ladner 1979; Pratt, 1979)
1対1モデル性
- 任意の充足可能な式が1対1モデルで満足される.
- 1対1モデル : 構造Sが1対1であるとは任意の原子プログラムAについて関係
が1対1であること
- Second order theory of n successors
- SnSへの変換が素直に与えられる条件:
そのモデルをグラフから木に変換できるような論理 - 決定可能
- 決定可能性の証明は無限木上のオートマトンのemptinessへの帰着による
PDL
- regular programにおける無限ループの概念を捉えるのに十分な力を持っていない(Pratt, 1978)
- 有限モデル性を満たす
PDL+natural formula construct (?)
- Propositional Algorithmic Logic (Mirkowska, 1980)のすべての式を表現可能
- Temporal Logic of Branching Time (Ben-Ari, Manna and Pnueli, 1981)のすべての式を表現可能
- 無限ループのpropositionalな概念を表現可能
PDL with Looping
- 状態のマージによって無限モデルから有限モデルへと縮小することのできない式が存在する(=>PDLより真に表現力が高い)
- 決定可能
- SnSへの埋め込みにより決定可能性を証明できるが、complexityの上界がelementaryでない(SnSがelementary timeで決定可能でない(Mayer, 1974))
- (少し弱い)有限モデル性を満たす(Street, 1980, 1982)
- モデルをグラフから木にできる(下位ノードにしか繋がっていない)
- elementary timeでの決定手続きは, SnSを経由せず無限木上のオートマトンのemptinessに直接帰着させることで得られる(Streett 1980, 1982)
- 1対1モデル性を満たす
PDL with converse
- PDLと同じ有限モデル性を満たす
- 決定手続き(Fischer and Ladner, 1979; Pratt, 1979)
- converse の構成についてのSnSへの自明な変換はまだ無い
- 1対1モデル性を満たさない
PDL with looping and converse
- 有限モデル性を満たさない(任意の有限モデルで充足可能でない式が存在する)
- しかし、決定可能(elementary decidable)
- グラフから木へと解こうとする際に, converseのせいでプログラムが任意のノードとつながってしまうため無限木上のオートマトンのemptinessへ帰着できない.(有限モデル性を満たさない理由)
- deterministic two way automata on infinite treeを使えば決定可能性を言える.
SOAPL (Second Order Acyclic Process Logic)
- 決定可能(SnSへの埋め込みによる)
- モデルをグラフから木にできる(下位ノードにしか繋がっていない)
参考文献
Pratt, 1978
Application of modal logic to programming | SpringerLink
Parikh, 1978
A decidability result for a second order process logic - IEEE Xplore Document
Propositional dynamic logic of looping and converse is elementarily decidable
http://ruthenia.info/txt/pavlo/03B/harel_kozen_tiuryn_2000.pdf
