Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version)
This work addresses model-checking and planning for data-aware processes, offering a compromise solution for satisfiable instances despite general undecidability, but it is incremental as it builds on existing LTLf and SMT frameworks.
The paper tackles the problem of extending Linear Temporal Logic over Finite Traces (LTLf) with first-order formulas over arbitrary theories, resulting in LTLf Modulo Theories (LTLfMT), which is semi-decidable. It provides a sound and complete semi-decision procedure implemented in the BLACK tool, with experimental evaluation demonstrating feasibility on novel benchmarks.
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.