Self-stabilizing mutual exclusion on directed graphs

This paper investigates the complexity of self-stabilizing mutual exclusion protocols for distributed systems, where processors communicate through shared memory according to a strongly connected directed communication graph. Tchuente's approach of covering a network with one directed cycle is taken as point of departure. This protocol requires $O(n^{2n)$ states per processor together with some preprocessing. By coalescing states a protocol requiring only $O(n^2)$ states per processor---still requiring preprocessing---is derived. Finally two protocols based on spanning trees are considered. Combining these protocols with a self-stabilizing spanning tree protocol yields two $O(n^3 m)$---where $m$ is the maximal degree of a processor---states per processor protocols that require knowledge of processor identities. This report concludes with a full proof of the coalesced states protocol in Lamport's Temporal Logic of Actions.