Branching-Time Model Checking Gap-Order Constraint Systems

Issue title: Reachability Problems for Infinite State Systems

Guest editors: Parosh Aziz Abdulla, Stéphane Demri, Alain Finkel, Jérôme Leroux and Igor Potapov

Article type: Research Article

Authors: Mayr, Richard^{a; *} | Totzke, Patrick^b

Affiliations: [a] University of Edinburgh, UK. http://homepages.inf.ed.ac.uk/rmayr/ | [b] University of Warwick, UK. http://www.dcs.warwick.ac.uk/~totzke/

Correspondence: [*] Address for correspondence: University of Edinburgh, 10 Crichton Street, Edinburgh EH8 9AB, UK.

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

DOI: 10.3233/FI-2016-1317

Journal: Fundamenta Informaticae, vol. 143, no. 3-4, pp. 339-353, 2016