Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version)
Abstract
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.
Keywords
Cite
@article{arxiv.2204.13693,
title = {Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version)},
author = {Luca Geatti and Alessandro Gianola and Nicola Gigante},
journal= {arXiv preprint arXiv:2204.13693},
year = {2022}
}
Comments
Extended version of a conference paper accepted at the 31st International Joint Conference on Artificial Intelligence (IJCAI-ECAI 2022)