A note on K-state self-stabilization in a ring with K=N

We show that, contrary to common belief, Dijkstra's K-state mutual exclusion algorithm on a ring [1, 2] 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 [8]. We show that K=N is sharp by giving a counter-example for K=N-1.