A Unified Automata-Theoretic Approach to LTLf Modulo Theories (Extended Version)

TL;DR

This work introduces a unified automata-theoretic framework for LTL_f modulo theories ($\text{LTL}_f^{\mathrm{MT}}$) by translating data-word properties into Symbolic Data-Word Automata (Sdwas) whose transitions are theory-guarded. The key insight is that Sdwas, though potentially undecidable for emptiness, can be reduced to solvable constrained Horn clause (CHC) systems, allowing the use of mature SMT/CHC solvers for satisfiability, model checking, and runtime monitoring. The authors provide a three-step automata-theoretic construction to obtain a deterministic Sdwa from any $\text{LTL}_f^{\mathrm{MT}}$ formula, enabling a practical, solver-friendly pipeline. Empirical results show the CHC-based approach matches or exceeds prior custom solutions in satisfiability tasks and extends naturally to model checking and monitoring. The framework thus offers a principled, scalable path for reasoning about data-rich temporal specifications in infinite-state systems, with potential for broader future integrations with additional logics and data theories.

Abstract

We present a novel automata-based approach to address linear temporal logic modulo theory (LTL-MT) as a specification language for data words. LTL-MT extends LTL_f by replacing atomic propositions with quantifier-free multi-sorted first-order formulas interpreted over arbitrary theories. While standard LTL_f is reduced to finite automata, we reduce LTL-MT to symbolic data-word automata (SDWAs), whose transitions are guarded by constraints from underlying theories. Both the satisfiability of LTL-MT and the emptiness of SDWAs are undecidable, but the latter can be reduced to a system of constrained Horn clauses, which are supported by efficient solvers and ongoing research efforts. We discuss multiple applications of our approach beyond satisfiability, including model checking and runtime monitoring. Finally, a set of empirical experiments shows that our approach to satisfiability works at least as well as a previous custom solution.

Figures (1)

• Figure 1: Architecture of the prototype implementation. Dashed transformations are performed manually.

Theorems & Definitions (19)

• Example 1
• Theorem 1
• Lemma 1
• proof
• Lemma 2
• proof
• Definition 1
• Theorem 2: Closure under Intersection
• Theorem 3: Emptiness
• Theorem 4