LTL式からBuchiオートマトンへの変換

読んだ論文についてメモ.

1.Fast LTL to Buchi Automata Translation

  • LTL -> Alternating Buchi Automata -> Generalized Buchi Automata -> Buchi Automata

ABAからGBAへの変換はABAがvery weakという性質を持つために可能らしい.
各ステップでオートマトンのサイズを小さくするために単純な簡約を行なっている.
この論文の実装はLTL2BAというツールとして公開されている.

2.Efficient Buchi Automata from LTL Formulae

  • LTL -> GBA -> BA

オートマトンのサイズを小さくするために,単純な式の書き換え,式を分解してDNFにした後ヒューリスティックに式を小さくする(0-1 ILPになるらしいけど謎),オートマトンを生成後単純化を行う,という3つのことをやっている.
オートマトンの単純化として,

  • direct simulation relation, reverse simulation relationを使って等価な状態を消す
  • GBAにおいて,受理条件が満たされるような強連結成分(fair SCC)に到達できないような状態を全て消す
  • GBAがweakなら,BAへの変換が単純にできる

3.Constructing Automata from Temporal Logic Formulas : A Tutorial

  • LTL -> GBA -> BA

オートマトンの各状態がtemporal formulaだけでなくリテラルも持つような構成法.チュートリアルだけあって,証明もわかりやすい.式の分解は集合的な手続きになっている.
リテラルを状態ではなく遷移に持たせることについても最後に少し書いてある.
GBAからBAへの変換は,1のものよりシンプル.

4.An Automata-Theoretic Approach to Linear Temporal Logic

  • LTL -> ABA -> BA

効率は良くない.LTLからBAへの変換以外にも色々と基本的なことが書かれている.
Nondeterministic BAとDeterministic BAの表現力の違い,NBAからRabin Automatonへの変換,NBAの空判定と充足可能性,Relaizability problemをRabin Tree Automatonの空判定として解く.
VardiさんのAn Automata-Theoretic Approachシリーズは他にもあるようなので勉強のために読みたい.