Branching-Time Model Checking Gap-Order Constraint Systems (Extended Version)

TL;DR

This paper investigates the model checking problem for Gap-order Constraint Systems (GCS) with respect to CTL, revealing undecidability for some fragments and decidability for others, impacting equivalence checking.

Contribution

It establishes the undecidability of EG model checking for GCS and the decidability of EF, advancing understanding of GCS verification.

Findings

EG model checking is undecidable for GCS.

EF model checking is decidable for GCS.

Decidability of bisimulation equivalence between GCS and finite-state systems.

Abstract

We consider the model checking problem for Gap-order Constraint Systems (GCS) w.r.t. the branching-time temporal logic CTL, and in particular its fragments EG and EF. GCS are nondeterministic infinitely branching processes described by evolutions of integer-valued variables, subject to Presburger constraints of the form $x-y\ge k$, where $x$ and $y$ are variables or constants and $k\in\mathbb{N}$ is a non-negative constant. We show that EG model checking is undecidable for GCS, while EF is decidable. In particular, this implies the decidability of strong and weak bisimulation equivalence between GCS and finite-state systems.