The Community for Technology Leaders
2010 17th International Symposium on Temporal Representation and Reasoning (TIME 2010) (2010)
Paris
Sept. 6, 2010 to Sept. 8, 2010
ISSN: 1530-1311
ISBN: 978-1-4244-8014-2
pp: 43-50
ABSTRACT
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.
INDEX TERMS
Boolean functions, computability, constraint handling, decidability, reachability analysis, temporal logic
CITATION

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.
doi:10.1109/TIME.2010.21
90 ms
(Ver 3.3 (11022016))