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$的自禁用进程组成的参数化对称单向环,存活锁检测是\emph{多项式时间可判定的}。给定一个由局部转移集合$T$指定的协议,该算法判定对于\emph{某些}环大小$K\!\geq\!2$是否存在存活锁,其运行时间为$O(|T|^3)$且与$K$无关。该算法计算有限集合$T$上紧缩单调算子的最大不动点,当且仅当该不动点非空时返回\emph{存活锁}。存活锁自由论点基于极大性:不动点是所有能够共同在每个进程上维持伪存活锁的最大转移集合;其空性直接证明对所有$K$均无存活锁,无需搜索环大小。该工作基于Farahat~\citep{farahat2012}对存活锁的代数刻画,该刻画建立了存活锁存在的充分必要条件,但未涉及可判定性。我们还处理了$(1,1)$-非对称情况,即一个特殊进程$P_0$与其余$K\!-\!1$个相同进程不同。代码和代数基础见URL:https://github.com/cosmoparadox/mathematical-tools。