Mayr, Richard; Totzke, Patrick Branching-time model checking gap-order constraint systems. (English) Zbl 1362.68176 Fundam. Inform. 143, No. 3-4, 339-353 (2016). Summary: 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 \geq 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. Cited in 1 Document MSC: 68Q60 Specification and verification (program logics, model checking, etc.) 03B25 Decidability of theories and sets of sentences 03B44 Temporal logic 68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) PDFBibTeX XMLCite \textit{R. Mayr} and \textit{P. Totzke}, Fundam. Inform. 143, No. 3--4, 339--353 (2016; Zbl 1362.68176) Full Text: DOI arXiv