论文标题
有限轨迹上的一阶时间逻辑：语义属性，可决定的片段和应用
First-order Temporal Logic on Finite Traces: Semantic Properties, Decidable Fragments, and Applications
论文作者
论文摘要
基于根据有限的严格线性订单解释的时间逻辑的形式主义（文献中称为有限痕迹）已被用于自动化计划，过程建模，（运行时）程序的验证和合成程序以及知识表示和推理的时间规范。在本文中，我们专注于有限轨迹的一阶时间逻辑。我们首先通过提供一组语义和句法条件来确保何时在两种情况下的推理之间的区别时，我们首先研究有限痕迹和无限痕迹之间公式的等价和满足性。此外，我们表明，对于一阶时间逻辑的几个可确定片段的有限痕迹上的可满足性问题是expspace-complete，就像无限的痕量案例一样，而当考虑有限的瞬间界限时，它会减少到nexptime。这也导致时间描述有限痕迹的逻辑的新复杂性结果。最后，我们研究了对计划和验证的申请，特别是通过与文献中对无敏感和安全性的不敏感的联系建立联系。
Formalisms based on temporal logics interpreted over finite strict linear orders, known in the literature as finite traces, have been used for temporal specification in automated planning, process modelling, (runtime) verification and synthesis of programs, as well as in knowledge representation and reasoning. In this paper, we focus on first-order temporal logic on finite traces. We first investigate preservation of equivalences and satisfiability of formulas between finite and infinite traces, by providing a set of semantic and syntactic conditions to guarantee when the distinction between reasoning in the two cases can be blurred. Moreover, we show that the satisfiability problem on finite traces for several decidable fragments of first-order temporal logic is ExpSpace-complete, as in the infinite trace case, while it decreases to NExpTime when finite traces bounded in the number of instants are considered. This leads also to new complexity results for temporal description logics over finite traces. Finally, we investigate applications to planning and verification, in particular by establishing connections with the notions of insensitivity to infiniteness and safety from the literature.
