Branching-time model checking gap-order constraint systems

DOI10.3233/FI-2016-1317MaRDI QIDQ2968527zbMATH OpenOpenAlexFDO

Authors Patrick Totzke, Richard M. Mayr

Publication date 16 March 2017

Published in Fundamenta Informaticae (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1307.4207

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Temporal logic (03B44) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

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-ygek$, where $x$ and $y$ are variables or constants and $kinmathbbN$ 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.

Recommendations

• Branching-time model checking gap-order constraint systems
• Verification of gap-order constraint abstractions of counter systems
• Verification of gap-order constraint abstractions of counter systems
• Branching-Time Temporal Logic Extended with Qualitative Presburger Constraints
• Strong termination for gap-order constraint abstractions of counter systems

Cited in

(7)

• CTL* model checking for data-aware dynamic systems with arithmetic
• Verification of gap-order constraint abstractions of counter systems
• Strong termination for gap-order constraint abstractions of counter systems
• Verification of gap-order constraint abstractions of counter systems
• Branching-time model checking gap-order constraint systems
• Constraint automata on infinite data trees: from \(\mathrm{CTL}(\mathbb{Z})/\mathrm{CTL}^*(\mathbb{Z})\) to decision procedures
• Constraint automata on infinite data trees: from CTL\((\mathbb{Z})\text{CTL}^*(\mathbb{Z})\) to decision procedures

This page was built for publication: Branching-time model checking gap-order constraint systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2968527)