Parameterized Model Checking of Token-Passing Systems

DOI10.1007/978-3-642-54013-4_15MaRDI QIDQ2938070zbMATH OpenOpenAlexFDO

Authors Benjamin Aminof, Swen Jacobs, Ayrat Khalimov, Sasha Rubin

Publication date 13 January 2015

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: We revisit the parameterized model checking problem for token-passing systems and specifications in indexed $$. Emerson and Namjoshi (1995, 2003) have shown that parameterized model checking of indexed $$ in uni-directional token rings can be reduced to checking rings up to some emph{cutoff} size. Clarke et al. (2004) have shown a similar result for general topologies and indexed $$, provided processes cannot choose the directions for sending or receiving the token. We unify and substantially extend these results by systematically exploring fragments of indexed $$ with respect to general topologies. For each fragment we establish whether a cutoff exists, and for some concrete topologies, such as rings, cliques and stars, we infer small cutoffs. Finally, we show that the problem becomes undecidable, and thus no cutoffs exist, if processes are allowed to choose the directions in which they send or from which they receive the token.

Recommendations

• Model checking parameterised multi-token systems via the composition method
• Model checking parameterized systems
• Parameterized compositional model checking
• Refinement checking on parametric modal transition systems
• scientific article; zbMATH DE number 1953016
• Parametric model checking with VerICS
• scientific article; zbMATH DE number 2086592
• Regular Model Checking Without Transducers (On Efficient Verification of Parameterized Systems)
• Unconventional Computation

Cited in

(22)

• Parameterised verification for multi-agent systems
• CONCUR 2004 - Concurrency Theory
• Parameterized model-checking of discrete-timed networks and symmetric-broadcast systems
• Model and program repair via group actions
• Round- and context-bounded control of dynamic pushdown systems
• Model and program repair via group actions and structure unwinding
• A counter abstraction technique for verifying properties of probabilistic swarm systems
• Parameterized model checking of rendezvous systems
• Parameterized model checking of rendezvous systems
• Verification of parameterized communicating automata via split-width
• Model checking parameterised multi-token systems via the composition method
• Verification of agent navigation in partially-known environments
• Parameterized model checking of networks of timed automata with Boolean guards
• Computer Science Logic
• Parameterized Verification of Communicating Automata under Context Bounds
• Liveness of parameterized timed networks
• Parameterized verification of time-sensitive models of ad hoc network protocols
• Phase-bounded broadcast networks over topologies of communication
• scientific article; zbMATH DE number 7559502 (Why is no real title available?)
• Automatic WSTS-based repair and deadlock detection of parameterized systems
• An automata-theoretic approach to the verification of distributed algorithms
• Nash equilibria in symmetric graph games with partial observation

This page was built for publication: Parameterized Model Checking of Token-Passing Systems

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