QSM-Cutoff: Systematic Derivation of Quantified Cutoff Formulas for Distributed Protocols

Abstract We introduce , a new procedure that employs the quantified symmetric minimization algorithm from [12] to systematically derive quantified formulas that precisely capture the onset of cutoff and saturation in distributed protocols. performs symmetry-aware forward reachability to enumerate the reachable states of a finite protocol instance, and applies symmetry-preserving logic minimization to express these states as a minimum-cost finitely-quantified reachability formula. repeats this finite analysis process to derive a sequence of reachability formulas $R_1, R_2, R_3, \cdots$ R 1 , R 2 , R 3 , ⋯ at increasing protocol sizes. This process terminates at size k when $R_k$ R k is a unique solution to symmetric minimization that yields the exact set of reachable states when evaluated at size $k+1$ k + 1 . We define $c:=k$ c : = k as the cutoff size and $R_c:=R_k$ R c : = R k as the cutoff formula . Empirically, $R_c$ R c is shown to be a reachability invariant that encodes the reachable states for any protocol size. extends the finite analysis process in [12] by introducing two algorithmic enhancements: a depth-first search algorithm that enumerates the reachable states of a finite protocol by searching only for their symmetric quotient, and an extended quantification pattern inference algorithm that expresses explicit clause orbits of finite instances by logically equivalent quantified formulas. Empirical results demonstrate that, compared to the techniques used in [12], is able to analyze a larger corpus of protocols, derive more compact quantified inductive invariants, and converge at smaller cutoffs. In contrast to previous scholarship, offers a new angle for understanding the notions of cutoff and saturation of distributed protocols. In particular, it raises intriguing questions about the unexpected role of symmetric logic minimization in this much-researched area and opens new directions for further research.