Linear temporal logic to Büchi automaton とは

正式検証では、有限状態モデル検査は、LTL公式およびBAが同じω言語を認識するように、所与の線形時間論理(LTL)公式に相当するBüchiオートマトン(BA)を見つける必要がある。 LTLの式をBAに変換するアルゴリズムがあります。この変換は通常2つのステップで行われます。最初のステップでは、LTL式から一般化されたBüchiオートマトン(GBA)を生成します。第2のステップは、このGBAをBAに変換します。 LTLはBAよりも表現力が厳密ではないので、逆の構成は不可能である。
LTLをGBAに変換するためのアルゴリズムは、それらの構築戦略において異なるが、それらはすべて共通の基礎原則を有する、すなわち、構築されたオートマトンにおける各状態は、状態の発生後に残りの入力語によって満たされると予想されるLTL式実行中に。