We prove that livelock detection is \emph{decidable in polynomial time} for parameterized symmetric unidirectional rings of self-disabling processes with bounded domain $\mathbb{Z}_m$. Given a protocol specified by its set of local transitions $T$, the algorithm decides whether a livelock exists for \emph{some} ring size $K\!\geq\!2$, running in $O(|T|^3)$ time independent of $K$. The algorithm computes the greatest fixed point of a deflationary monotone operator on the finite set $T$ and returns \emph{livelock} iff the fixed point is non-empty. The livelock freedom argument rests on maximality: the fix-point is the largest set of transitions that can together sustain a pseudolivelock at every process; its emptiness certifies freedom for all $K$ without any search over ring sizes. The work is grounded in the algebraic characterization of livelocks from Farahat~\citep{farahat2012}, which establishes necessary and sufficient conditions for livelock existence but does not address decidability. We also handle the $(1,1)$-asymmetric case in which one distinguished process $P_0$ differs from the remaining $K\!-\!1$ identical processes. Code and algebraic foundation are at the URL: https://github.com/cosmoparadox/mathematical-tools.
翻译:我们证明:对于具有有界域$\mathbb{Z}_m$的参数化对称自禁用进程单向环,活锁检测是**多项式时间可判定的**。给定由其局部转移集合$T$指定的协议,该算法无需搜索环大小$K\!\geq\!2$,即可在$O(|T|^3)$时间内判定是否存在针对**某个**环大小的活锁。该算法通过计算有限集$T$上单调减算子的最大不动点,并仅在不动点非空时判定存在**活锁**。无活锁论证基于极大性:该不动点是能共同在每个进程维持伪活锁的最大转移集合;其空性保证了所有$K$下均无活锁,无需遍历环大小进行搜索。本工作基于Farahat等人~[2012]对活锁的代数刻画,该刻画给出了活锁存在的充要条件但未涉及可判定性。我们还处理了$(1,1)$-非对称情形:即一个特殊进程$P_0$与其余$K\!-\!1$个相同进程不同。代码及代数基础见链接:https://github.com/cosmoparadox/mathematical-tools。