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

arXiv: https://arxiv.org/abs/1307.4207 · HTML: https://mlsanity.com/paper/1307.4207/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 16 Jul 2013.

## Built on by (most cited first, 1 of 1)

- [Linear-Time Verification of Data-Aware Dynamic Systems with Arithmetic](https://mlsanity.com/paper/2203.07982/) (2022)

## Abstract (arXiv)

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≥ k, where x and y are variables or constants and k∈mathbbN 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.