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

要約

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