Branching-Time Model Checking Gap-Order Constraint Systems

Richard Mayr, Patrick Totzke

Research output: Contribution to journalArticlepeer-review

Abstract / Description of output

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 in 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.
Original languageEnglish
Pages (from-to)339-353
Number of pages15
JournalFundamenta Informaticae
Volume143
Issue number3-4
Early online date25 Feb 2015
DOIs
Publication statusPublished - 29 Aug 2015

Keywords / Materials (for Non-textual outputs)

  • Model checking
  • Gap-order Constraint systems

Fingerprint

Dive into the research topics of 'Branching-Time Model Checking Gap-Order Constraint Systems'. Together they form a unique fingerprint.

Cite this