Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

42

FUIN
2016

favoriteEmaildiscussreport

60views more FUIN 2016»

Branching-Time Model Checking Gap-Order Constraint Systems

8 years 7 months ago

Branching-Time Model Checking Gap-Order Constraint Systems

Download www.dcs.warwick.ac.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 inﬁnitely 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 ∈ 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 ﬁnite-state systems.

Richard Mayr, Patrick Totzke

Real-time Traffic

FUIN 2016 |

claim paper

Related Content

» Model Checking Games for a Fair BranchingTime Temporal Epistemic Logic

» Learning to verify branching time properties

» Bounded model checking knowledge and branching time in synchronous multiagent systems

» The Complexity of Epistemic Model Checking Clock Semantics and Branching Time

» CacheBased Model Checking of Networked Applications From Linear to Branching Time

» BranchingTime Property Preservation Between RealTime Systems

» BranchingTime Temporal Logics with Minimal Model Quantifiers

» Partial Order Reduction for Probabilistic Branching Time

» Parallel Model Checking for Temporal Epistemic Logic

» On Reduction Criteria for Probabilistic Reward Models

Post Info
More Details (n/a)

Added	03 Apr 2016
Updated	03 Apr 2016
Type	Journal
Year	2016
Where	FUIN
Authors	Richard Mayr, Patrick Totzke

Comments (0)