We revisit the decidability of livelock detection in self-disabling unidirectional ring protocols, a problem shown to be undecidable in general by Klinkhamer and Ebnenasir via reduction from the periodic domino problem. Despite this, practical protocols routinely admit finite proofs of livelock freedom via the same tiling constraints, and synthesis of parameterized self-stabilizing rings has been shown to be decidable -- suggesting a gap between theory and practice. We identify the source of this gap: the apparent unboundedness of livelock reasoning is an artifact of working in the transition space. By lifting to an \emph{equivariant product space} -- the space of transition-witness pairs coupled by the zigzag equivariance conditions of Farahat -- we show that self-disabling induces a structure in which closure and period are preserved under backward propagation. This yields a bounded witness property: every livelock, constructed from a set of local transitions $T$, admits a representative as a local cycle of length at most $|T|^2$ in a finite product graph, independent of the ring size. We derive a sound and complete decision procedure via greatest fixed-point iteration on the product graph. Our results demonstrate that decidability emerges not by restricting the problem syntactically, but by exposing its underlying finite combinatorial structure. We validate on over 4,300 protocols with zero errors, extend to $(1,1)$-asymmetric protocols, and derive a circulation law classifying livelocks by ring size. Code and algebraic foundation are at the URL https://github.com/cosmoparadox/mathematical-tools.

翻译：暂无翻译