Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version)
| Autor: | Geatti, Luca, Gianola, Alessandro, Gigante, Nicola |
|---|---|
| Rok vydání: | 2022 |
| Předmět: | |
| Druh dokumentu: | Working Paper |
| Popis: | 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. Comment: Extended version of a conference paper accepted at the 31st International Joint Conference on Artificial Intelligence (IJCAI-ECAI 2022) |
| Databáze: | arXiv |
| Externí odkaz: |
|