Tight Cutoffs for Guarded Protocols with Fairness

TL;DR

This paper extends cutoff results for guarded protocols to open systems with fairness assumptions, enabling scalable verification of liveness properties and deadlock detection in parameterized systems.

Contribution

It introduces new cutoff results for open guarded protocols with fairness, addressing limitations of previous results for liveness and deadlock detection.

Findings

New cutoff results for open systems with fairness

Cutoffs for detecting global and local deadlocks

Proved tightness or asymptotic tightness of cutoffs

Abstract

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.