Bounded Reachability for Temporal Logic over Constraint Systems

TL;DR

This paper introduces CLTLB(D), an extension of temporal logic with constraints, and provides conditions under which bounded reachability and satisfiability are decidable, along with an effective decision procedure.

Contribution

It extends PLTLB with constraints over system D and identifies restrictions that ensure decidability of satisfiability and bounded reachability.

Findings

Decidability of satisfiability for CLTLB(D) under certain restrictions.

An encoding for bounded reachability that enables effective decision procedures.

Applicability to a large class of 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.