2024/08/16 by Marco Faella, Faella, Marco, Gennaro Parlato +1
Computer Science · #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #semigroups and automata theory
paper · pdf · doi:10.48550/arxiv.2408.08817
openalex publication_date 2024/08/16 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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 LTLf by replacing atomic propositions with quantifier-free multi-sorted first-order formulas interpreted over arbitrary theories. While standard LTLf 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.