Another Look at LTL Modulo Theory over Finite and Infinite Traces

Linear Temporal Logic is a de facto standard for specification of properties of complex systems. Fundamental problems in formal verification include satisfiability checking and model checking. Extensions and variants of LTL have gained significant interest: with LTLf, the temporal formulas are interpreted over finite traces; with safety fragments of LTL, model checking can be reduced to search for finite trace counterexamples; in the context of Verification Modulo Theories, LTL includes first-order atoms interpreted over background theories. In this paper we propose a symbolic, automata-theoretic approach for these variants of LTL in a general and comprehensive framework, show the correctness of the reduction to liveness and invariant checking, and present a library of open benchmarks and support tools.