A first-order logic characterization of safety and co-safety languages

要約

線形時相論理 (LTL) は最も人気のある時相論理の 1 つであり、コンピューター サイエンスのさまざまな分野で活用されています。
その広範な使用のさまざまな理由の中には、その強力な基本特性があります。LTL は、カウンターフリーのオメガ オートマトン、スターフリーのオメガ正規表現、および (カンプの定理による) 線形順序の一次理論と同等です。
(FO-TLO)。
セーフティ言語とコセーフティ言語は、それぞれ単語がその言語に属さないかどうかを確立するために十分な有限の接頭辞で十分であり、LTL のモデル チェックやリアクティブ合成などの問題の複雑さを軽減する上で重要な役割を果たします。
SafetyLTL (または coSafetyLTL) は、ユニバーサル (または存在) 時間モダリティのみが許可され、安全 (または co-safety) 言語のみを認識する LTL のフラグメントです。
この論文の主な貢献は、SafetyFO と呼ばれる FO-TLO のフラグメントとそのデュアル coSafetyFO の導入です。これらは、LTL で定義可能なセーフティおよびコセーフティ言語に関して表現的に完全です。
我々は、それらがそれぞれ SafetyLTL と coSafetyLTL を正確に特徴づけていることを証明します。これはカンプの定理に加わる結果であり、一次言語の観点から LTL (の断片) の特徴づけをより明確に示すものです。
さらに、LTL で定義可能な安全言語は SafetyLTL でも定義できるという、直接的でコンパクトな自己完結型の証明が得られます。
副産物として、有限ワードと無限ワードで解釈された SafetyLTL の弱い明日演算子の表現力に関する興味深い結果が得られます。
さらに、有限の単語にわたって解釈された場合、明日 (または弱い明日) 演算子のない SafetyLTL (または coSafetyLTL) が、有限の単語にわたる LTL の安全 (または co-safety) フラグメントをキャプチャすることを証明します。

要約(オリジナル)

Linear Temporal Logic (LTL) is one of the most popular temporal logics, that comes into play in a variety of branches of computer science. Among the various reasons of its widespread use there are its strong foundational properties: LTL is equivalent to counter-free omega-automata, to star-free omega-regular expressions, and (by Kamp’s theorem) to the First-Order Theory of Linear Orders (FO-TLO). Safety and co-safety languages, where a finite prefix suffices to establish whether a word does not belong or belongs to the language, respectively, play a crucial role in lowering the complexity of problems like model checking and reactive synthesis for LTL. SafetyLTL (resp., coSafetyLTL) is a fragment of LTL where only universal (resp., existential) temporal modalities are allowed, that recognises safety (resp., co-safety) languages only. The main contribution of this paper is the introduction of a fragment of FO-TLO, called SafetyFO, and of its dual coSafetyFO, which are expressively complete with respect to the LTL-definable safety and co-safety languages. We prove that they exactly characterize SafetyLTL and coSafetyLTL, respectively, a result that joins Kamp’s theorem, and provides a clearer view of the characterization of (fragments of) LTL in terms of first-order languages. In addition, it gives a direct, compact, and self-contained proof that any safety language definable in LTL is definable in SafetyLTL as well. As a by-product, we obtain some interesting results on the expressive power of the weak tomorrow operator of SafetyLTL, interpreted over finite and infinite words. Moreover, we prove that, when interpreted over finite words, SafetyLTL (resp. coSafetyLTL) devoid of the tomorrow (resp., weak tomorrow) operator captures the safety (resp., co-safety) fragment of LTL over finite words.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google