Konsep Inti
LTLからCOCOAへの直接的な変換手順を提案し、LTLからパリティ自動機への変換にも応用できる。この変換手順は自然色の定義を活用し、従来の複雑な構成を回避できる。
Abstrak
本論文では、LTLからCOCOAへの直接的な変換手順を提案している。COCOAは最近導入された新しい正則言語の標準表現で、各ω語に自然色を割り当てる。しかし、LTLからCOCOOAへの変換は現在のところ、LTLからパリティ自動機への変換を経由する複雑な手順しか知られていない。
提案する変換手順は以下の通り:
入力のLTL式をweakな交替自動機に変換する。
義務グラフを構築し、これを用いて接尾語言語を追跡するマシンを定義する。
義務グラフの初期状態集合を最大化する。
拡張部分集合構成を適用し、最初のCOCOA自動機A1を構築する。
一般のレベルℓ>1のCOCOA自動機Aℓを構築する。
この変換手順は、自然色の定義を活用することで、従来の複雑な構成を回避できる。また、パリティ自動機への変換にも応用できる。変換は漸化的に最適な二重指数時間で行われ、生成される自動機のサイズも漸化的に最適である。
Statistik
提案する変換手順は漸化的に最適な二重指数時間で動作する。
生成される自動機のサイズも漸化的に最適である。