Pnueli論文のメモ

研究 主テーマ

MSCのライバルMTS(Modal Transition System)をやっているUchitelに対抗すべく
理論武装のため、合成派の古典論文であるPnueliの"On the synthesis of a reactive module"を読んだ。

リアクティブシステムは環境からの入力変数xに対して動作してyを環境に対して出力するものとして
このシステムのプロパティとしてφ(x,y)という性質をもつときに、このリアクティブシステムを
合成できるか？というのがお題で、環境とシステムの間のgameとみたてて、環境がどんな手xを繰り出しても
φ(x,y)が成立するようなyを出力できるようなプログラムが構築できるか？という課題に落とし込み、
これが、tree automaton問題になってさらに、transducer問題に帰着されて、最後にプログラムになる
という話（つながっているのか？？？？）

理解できていないが、忘れないために概要をメモする。

Theorem1.以下は同値である

  • 線形時相論理φが実装可能である
  • ψ=(∀x)(∃y)Aφ(x,y)が全てのtree modelに対してvalidである
  • Aφ(x,y)があるfull-x-treeで成り立つこと
  • あとは略

Theorem2.線形時相論理φを実装するプログラム(P=P^Cを構成するtransducer C)を得るためには、

  • 線形時相論理φからNondeterministic Buchi Automaton(NBA)を生成
    • standard constructionという手法が確立されているらしい。Tabulau法だったりなんだったり、
  • NBAをdeterministicなRabin Automaton:Bに変換
    • ここでいわゆるSafraの構成法がでてくる
  • Bを無限木上のtree-automaton B'と見立てる
  • Tω(B')のemptinessの検査をする
  • 上記検査の過程ででてきたtransducer Cがφを実装するプログラムである
    • boolean domainに限定すると以下の流れになる
    • Theorem1より、φ(x,y)が実装可能であることとAφ(x,y)がsome full-x-treeで成立することが同値であることを利用すると
    • full binary tree でφ(x,y)が常に成立するようなラベリングL(s,x),L(s,y)を求めればよい
    • L(s,x)はfull-x-treeできまるので、L(s,y)をきめればよい
    • すなわちL(s,y)がφ(x,y)を成立させるように割り当てられたbinary treeを受理するTree Automaton Aをつくればよい
    • ψの全てのtree modelにおいてvalid性は、Tω(A)のnon-emptinessに帰着できることが知られており
    • さらに[HR72,Rab72]であるように、t.a. A がある無限の木を受理するiff Aがあるregular-labellingを受理する
    • regular labeling はdeterministic (string) ω-transducerにより生成できる
    • transducerは0,1にエンコードされたdirectionのシーケンスを入力として、木をたどり、各ノードでlabelを出力する
    • このようなtransducer Cが見つかれば、P=P^Cとなるプログラムとして解釈できる
      • P=P^Mって、"fpM(a0,a1,...,ai)=L(a0,a1,...,ai,y)"(p184)のこと？？
    • このプログラムは変数xの履歴a1,...,akを入力として、yをポイントポイントで出力する。