Bounded Reachability for Temporal Logic over Constraint Systems

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.

References in corpus (4)

• Linear Encodings of Bounded LTL Model Checking
• A Metric Encoding for Bounded Model Checking (extended version)
• Integrated Modeling and Verification of Real-Time Systems through Multiple Paradigms
• SMT-based Verification of LTL Specifications with Integer Constraints and its Application to Runtime Checking of Service Substitutability

Cited by in corpus (2)

• Reactive Integrated Mission and Motion planning
• Combined Top-Down and Bottom-Up Approaches to Performance-guaranteed Integrated Task and Motion Planning of Cooperative Multi-agent Systems