Tight cutoffs for guarded protocols with fairness

Simon Außerlechner, Swen Jacobs, Ayrat Khalimov

Research output: Chapter in Book/Report/Conference proceedingConference paperpeer-review


Guarded protocols were introduced in a seminal paper by Emerson and Kahlon (2000), and describe systems of processes whose transitions are enabled or disabled depending on the existence of other processes in certain local states. We study parameterized model checking and synthesis of guarded protocols, both aiming at formal correctness arguments for systems with any number of processes. Cutoff results reduce reasoning about systems with an arbitrary number of processes to systems of a determined, fixed size. Our work stems from the observation that existing cutoff results for guarded protocols (i) are restricted to closed systems, and (ii) are of limited use for liveness properties because reductions do not preserve fairness. We close these gaps and obtain new cutoff results for open systems with liveness properties under fairness assumptions. Furthermore, we obtain cutoffs for the detection of global and local deadlocks, which are of paramount importance in synthesis. Finally, we prove tightness or asymptotic tightness for the new cutoffs.
Original languageEnglish
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
PublisherSpringer Berlin - Heidelberg
Pages474 - 496
ISBN (Electronic)978-366249121-8
Publication statusPublished - 2016
Event17th International Conference on Verification, Model Checking, and Abstract Interpretation: VMCAI 2016 - St. Petersburg, Russian Federation
Duration: 17 Jan 201619 Jan 2016


Conference17th International Conference on Verification, Model Checking, and Abstract Interpretation
Country/TerritoryRussian Federation
CitySt. Petersburg

Fields of Expertise

  • Information, Communication & Computing


Dive into the research topics of 'Tight cutoffs for guarded protocols with fairness'. Together they form a unique fingerprint.

Cite this