Bounded Reachability for Temporal Logic over Constraint Systems
Authors:
- Marcello M. BersaniMBMarcello M. Bersani
- Achille FrigeriAFAchille Frigeri
- Angelo MorzentiAMAngelo Morzenti
- Matteo PradellaMPMatteo Pradella
- Matteo RossiMRMatteo Rossi
- Pierluigi San PietroPPPierluigi San Pietro
- 1 September 2010
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 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.Keywords
All Related Versions
This publication has 13 references indexed in Scilit:
- A Metric Encoding for Bounded Model Checking2009
- The symmetry of the past and of the future2007
- Linear Encodings of Bounded LTL Model CheckingLogical Methods in Computer Science, 2006
- Towards a Model-Checker for Counter SystemsLecture Notes in Computer Science, 2006
- LTL over Integer Periodicity ConstraintsLecture Notes in Computer Science, 2004
- An Automata-Theoretic Approach to Constraint LTLLecture Notes in Computer Science, 2002
- Flatness Is Not a Weakness2000
- Temporal and Modal Logic1990
- Complexity, convexity and combinations of theoriesTheoretical Computer Science, 1980
- On the temporal analysis of fairness1980