An automata-theoretic approach to constraint LTL (Q870361)

Building on their earlier paper [``An automata-theoretic approach to constraint LTL'', Lect. Notes Comput. Sci. 2556, 121--132 (2002; Zbl 1027.03027)], the authors consider an extension of the linear-time temporal logic LTL with constraints interpreted over a concrete domain and, using a new automata-theoretic technique, they show PSPACE-decidability of the logics for the constraint systems \((\mathbb{Z},<,=)\) and \((\mathbb{N},<,=)\). Notably, unlike the propositional LTL, the formulae of these constraint logics do not preserve \(\omega\)-regularity of the sets of models. Nevertheless, the authors succeed to approximate from above the set of models of every such formula with an \(\omega\)-regular superset that contains the same ultimately periodic words, thus reducing the non-emptiness problem of the former to the non-emptiness problem of the latter, whence the decidability results follow. The second main contribution is the modularity of the automata-theoretic technique developed in the paper, in the sense that the automaton constructed to check satisfiability of a given formula is the interstection of two separate automata, one corresponding to the underlying logical language, and the other to the considered constraint system. The authors demonstrate the benefits from this modular approach, in particular by extending the decision procedure to handle past operators added to LTL, as well as to full Büchi MSO over \(\mathbb{N}\) over the considered systems of constraints. Finally, the authors extend the decidability and complexity results to constraint systems with constants, by reduction to the standard case, while they show that adding a `counting' mechanism to the constraint system leads to undecidability.