# Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version)

arXiv: https://arxiv.org/abs/2204.13693 · HTML: https://mlsanity.com/paper/2204.13693/

## Key facts

- Cited by 8 papers in the map (data through 14 Oct 2026).
- Builds on 6 of its 51 references that are in the map.
- First posted on arXiv 28 Apr 2022.

## Builds on (most cited first, 6 of 6)

- [Information and Computation](https://mlsanity.com/paper/1304.1428/) (2013)
- [A New Rule for LTL Tableaux](https://mlsanity.com/paper/1609.04102/) (2016)
- [One-Pass and Tree-Shaped Tableau Systems for TPTL and TPTLb+Past](https://mlsanity.com/paper/1809.03101/) (2018)
- [VERIFAS: A Practical Verifier for Artifact Systems](https://mlsanity.com/paper/1705.10007/) (2017)
- [Formal Modeling and SMT-Based Parameterized Verification of Data-Aware BPMN (Extended Version)](https://mlsanity.com/paper/1906.07811/) (2019)
- [A Parallel Linear Temporal Logic Tableau](https://mlsanity.com/paper/1709.02101/) (2017)

## Built on by (most cited first, 8 of 8)

- [Decidable Fragments of LTLf Modulo Theories (Extended Version)](https://mlsanity.com/paper/2307.16840/) (2023)
- [Predictable and Performant Reactive Synthesis Modulo Theories via Functional Synthesis](https://mlsanity.com/paper/2407.09348/) (2024)
- [ScenicProver: A Framework for Compositional Probabilistic Verification of Learning-Enabled Systems](https://mlsanity.com/paper/2511.02164/) (2025)
- [Research Vision: Multi-Agent Path Planning for Cops And Robbers Via Reactive Synthesis](https://mlsanity.com/paper/2503.11475/) (2025)
- [Towards Constraint Temporal Answer Set Programming](https://mlsanity.com/paper/2507.13958/) (2025)
- [Do It for HER: First-Order Temporal Logic Reward Specification in Reinforcement Learning (Extended Version)](https://mlsanity.com/paper/2602.06227/) (2026)
- [Mining Beyond the Bools: Learning Data Transformations and Temporal Specifications](https://mlsanity.com/paper/2603.06710/) (2026)
- [Monitoring Data-aware Temporal Properties (Extended Version)](https://mlsanity.com/paper/2605.14666/) (2026)

## Abstract (arXiv)

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.