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.

翻译：本文研究“线性时空理论对有限追踪(LTLf)的线性时空逻辑(LTLf),用第一阶公式来取代“满足性莫杜洛理论”的精神对任意理论进行解释,由此得出的逻辑称为“LTLf Modulo理论”(LTLfMT)是半分数,然而,其高清晰度在许多使用案例中是有用的,如数据认知过程和数据认知规划的示范检查等。尽管这些问题一般是不可变的,但能够解决可比较的事例是一种值得研究的妥协。在对使用案例进行激励和描述后,我们为LTLTFMT提供了一种健全和完整的半决定程序,其依据是单行树形平板系统的SMT编码。这种算法在BLACK卫星兼容性检查工具中实施,实验性评估显示新基准方法的可行性。