Decidable Fragments of LTLf Modulo Theories (Extended Version)

要約

私たちは、有限トレース上の線形時相論理モジュロ理論 (LTLfMT) を研究します。これは、命題が一次式に置き換えられ、異なる時点を参照する一次変数を比較できる、有限トレース上の LTL (LTLf) の最近導入された拡張です。
一般に、LTLfMT は、タブローベースの半決定手順を使用して、決定可能な一次理論 (線形算術など) に対して半決定可能であることが示されています。
このペーパーでは、LTLfMT タブローのための健全で完全な枝刈りルールを紹介します。
有限メモリと呼ばれる抽象的で意味論的な条件を満たす LTLfMT 式については、新しいルールで強化されたタブローも終了することが保証されることを示します。
最後に重要なことですが、この手法を使用すると、LTLfMT のいくつかのフラグメントの充足可能性について新しい決定可能性の結果を確立できるだけでなく、既知のクラスに対して新しい決定可能性の証明を与えることができます。

要約(オリジナル)

We study Linear Temporal Logic Modulo Theories over Finite Traces (LTLfMT), a recently introduced extension of LTL over finite traces (LTLf) where propositions are replaced by first-order formulas and where first-order variables referring to different time points can be compared. In general, LTLfMT was shown to be semi-decidable for any decidable first-order theory (e.g., linear arithmetics), with a tableau-based semi-decision procedure. In this paper we present a sound and complete pruning rule for the LTLfMT tableau. We show that for any LTLfMT formula that satisfies an abstract, semantic condition, that we call finite memory, the tableau augmented with the new rule is also guaranteed to terminate. Last but not least, this technique allows us to establish novel decidability results for the satisfiability of several fragments of LTLfMT, as well as to give new decidability proofs for classes that are already known.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google