Branching-Time Model Checking Gap-Order Constraint Systems

Richard Mayr; Patrick Totzke

doi:10.1007/978-3-642-41036-9_16

Branching-Time Model Checking Gap-Order Constraint Systems

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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.

Original language	English
Title of host publication	Reachability Problems
Subtitle of host publication	7th International Workshop, RP 2013, Uppsala, Sweden, September 24-26, 2013 Proceedings
Publisher	Springer Berlin Heidelberg
Pages	171-182
Number of pages	12
ISBN (Electronic)	978-3-642-41036-9
ISBN (Print)	978-3-642-41035-2
DOIs	https://doi.org/10.1007/978-3-642-41036-9_16
Publication status	Published - 2013

Access to Document

10.1007/978-3-642-41036-9_16

Mayr Totzke 2013 Branching Time Model Checking Gap Order Contraint SystemsAccepted author manuscript, 316 KB

http://dx.doi.org/10.1007/978-3-642-41036-9_16

Cite this

@inproceedings{60ff8ba4e9d2423b9fa6905cf937b862,

title = "Branching-Time Model Checking Gap-Order Constraint 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 ≥ 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.",

author = "Richard Mayr and Patrick Totzke",

year = "2013",

doi = "10.1007/978-3-642-41036-9_16",

language = "English",

isbn = "978-3-642-41035-2",

pages = "171--182",

booktitle = "Reachability Problems",

publisher = "Springer Berlin Heidelberg",

}

TY - GEN

T1 - Branching-Time Model Checking Gap-Order Constraint Systems

AU - Mayr, Richard

AU - Totzke, Patrick

PY - 2013

Y1 - 2013

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-642-41036-9_16

DO - 10.1007/978-3-642-41036-9_16

M3 - Conference contribution

SN - 978-3-642-41035-2

SP - 171

EP - 182

BT - Reachability Problems

PB - Springer Berlin Heidelberg

ER -

Branching-Time Model Checking Gap-Order Constraint Systems

Abstract

Access to Document

Fingerprint

Cite this