We introduce QSM-Cutoff, 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. QSM-Cutoff 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. QSM-Cutoff repeats this finite analysis process to derive a sequence of reachability formulas \(R_1, R_2, R_3, \cdots \) at increasing protocol sizes. This process terminates at size k when \(R_k\) is a unique solution to symmetric minimization that yields the exact set of reachable states when evaluated at size \(k+1\) . We define \(c :=k\) as the cutoff size and \(R_c:=R_k\) as the cutoff formula. Empirically, \(R_c\) is shown to be a reachability invariant that encodes the reachable states for any protocol size. QSM-Cutoff 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], QSM-Cutoff 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, QSM-Cutoff 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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

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

  • Yun-Rong Luo,
  • Aman Goel,
  • Karem Sakallah

摘要

We introduce QSM-Cutoff, 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. QSM-Cutoff 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. QSM-Cutoff repeats this finite analysis process to derive a sequence of reachability formulas \(R_1, R_2, R_3, \cdots \) at increasing protocol sizes. This process terminates at size k when \(R_k\) is a unique solution to symmetric minimization that yields the exact set of reachable states when evaluated at size \(k+1\) . We define \(c :=k\) as the cutoff size and \(R_c:=R_k\) as the cutoff formula. Empirically, \(R_c\) is shown to be a reachability invariant that encodes the reachable states for any protocol size. QSM-Cutoff 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], QSM-Cutoff 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, QSM-Cutoff 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.