In: Desel, J.: Structures in Concurrency Theory, Proceedings of the International Workshop on Structures in Concurrency Theory (STRICT), Berlin, 11-13 May 1995, pages 205-219. 1995.
Abstract: We present a new solution of the mutual exclusion problem, which is modelled as a Petri net. In order to present a concise model of the algorithm, we extend Petri nets by the concepts of progress and nonprogress transitions and fair arcs. Moreover, we introduce a simple temporal logic in order to express and verify properties of distributed algorithms. The verification rules allow for rigorous reasoning close to the arguments of an informal proof. The verification method is applied to the new solution as well as to Peterson' s solution. This allows for a comparison of the two algorithms.