Bounded Reachability for Temporal Logic over Constraint Systems

This paper defines CLTLB(D), an extension of PLTLB (PLTL with both past and future operators) augmented with atomic formulae built over a constraint system D. The paper introduces suitable restrictions and assumptions that make the satisfiability problem decidable in many cases, although the problem is undecidable in the general case. Decidability is shown for a large class of constraint systems, and an encoding into Boolean logic is defined. This paves the way for applying existing SMT-solvers for checking the Bounded Reachability problem, as shown by various experimental results.