2010 17th International Symposium on Temporal Representation and Reasoning (TIME 2010) (2010)
Sept. 6, 2010 to Sept. 8, 2010
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TIME.2010.21
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.
Boolean functions, computability, constraint handling, decidability, reachability analysis, temporal logic
M. M. Bersani, A. Frigeri, A. Morzenti, M. Pradella, M. Rossi and P. San Pietro, "Bounded Reachability for Temporal Logic over Constraint Systems," 2010 17th International Symposium on Temporal Representation and Reasoning (TIME 2010)(TIME), Paris, 2010, pp. 43-50.