Verifying livelock freedom on parameterized rings and chains

Abstract

This paper investigates the complexity of verifying livelock freedom, self-stabilization, and weak stabilization in parameterized unidirectional ring and bidirectional chain topologies. Specifically, we illustrate that verifying livelock freedom of parameterized rings consisting of self-disabling and deterministic processes is undecidable (specifically, Π10-complete). This result implies that verifying self-stabilization and weak stabilization for parameterized rings of self-disabling processes is also undecidable. The results of this paper strengthen previous work on the undecidability of verifying temporal logic properties in symmetric ring protocols. The proof of undecidability is based on a reduction from the periodic domino problem. © Springer International Publishing 2013.