Nordic Journal of Computing A NOTE ON K-STATE SELF-STABILIZATION IN A RING WITH

Abstract. We show that, contrary to common belief, Dijkstra's K-state mutual exclusion algorithm on a ring also stabilizes when the number K of states per process is one less than the number N + 1 of processes in the ring. We formalize the algorithm and verify the proof in PVS, based on Qadeer and Shankar's work. We show that K = N is sharp by giving a counter-example for K = N 1