论文标题
有限迹线的线性时间逻辑模型理论（扩展版本）
Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version)
论文作者
论文摘要
本文研究了有限痕迹（LTLF）的线性时间逻辑，其中命题字母被以可满足的模型理论精神解释的一阶公式替换为一阶公式。所得的逻辑，称为LTLF Modulo理论（LTLFMT），是可以半确定的。然而，它的高表现力在许多用例中很有用，例如对数据感知过程和数据感知计划的模型检查。尽管这些问题普遍不可证明，但能够解决令人满意的实例还是值得研究的妥协。在激励和描述了此类用例之后，我们基于单通树形图表系统的SMT编码为LTLFMT提供了声音和完整的半决赛过程。该算法是在黑色满意度检查工具中实现的，实验评估显示了该方法对新基准测试的可行性。
This paper studies Linear Temporal Logic over Finite Traces (LTLf) where proposition letters are replaced with first-order formulas interpreted over arbitrary theories, in the spirit of Satisfiability Modulo Theories. The resulting logic, called LTLf Modulo Theories (LTLfMT), is semi-decidable. Nevertheless, its high expressiveness comes useful in a number of use cases, such as model-checking of data-aware processes and data-aware planning. Despite the general undecidability of these problems, being able to solve satisfiable instances is a compromise worth studying. After motivating and describing such use cases, we provide a sound and complete semi-decision procedure for LTLfMT based on the SMT encoding of a one-pass tree-shaped tableau system. The algorithm is implemented in the BLACK satisfiability checking tool, and an experimental evaluation shows the feasibility of the approach on novel benchmarks.
