Bounded Reachability for Temporal Logic over Constraint Systems
Preprint
Abstract
We present CLTLB(D), an extension of PLTLB (PLTL with both past and future operators) augmented with atomic formulae built over a constraint system D. Even for decidable constraint systems, satisfiability and Model Checking problem of such logic can be undecidable. We introduce suitable restrictions and assumptions that are shown to make the satisfiability problem for the extended logic decidable. Moreover for a large class of constraint systems we propose an encoding that realize an effective decision procedure for the Bounded Reachability problem.Keywords
All Related Versions
This publication has 8 references indexed in Scilit:
- SMT-based Verification of LTL Specification with Integer Constraints and its Application to Runtime Checking of Service Substitutability2010
- The Effects of Bounding Syntactic Resources on Presburger LTLJournal of Logic and Computation, 2009
- Refining Real-Time System Specifications through Bounded Model- and Satisfiability-Checking2008
- Linear Encodings of Bounded LTL Model CheckingLogical Methods in Computer Science, 2006
- Towards a Model-Checker for Counter SystemsLecture Notes in Computer Science, 2006
- Lazy Theorem Proving for Bounded Model Checking over Infinite Domains2002
- Multiple counters automata, safety analysis and presburger arithmetic1998
- Complexity, convexity and combinations of theoriesTheoretical Computer Science, 1980