In: Freksa, C.; Jantzen, M.; Valk, R.: Lecture Notes in Computer Science, Vol. 1337: Foundations of Computer Science: Potential - Theory - Cognition, pages 261-270. Springer-Verlag, 1997.
Abstract: Concise models of distributed algorithms which on one hand allow rigorous correctness proofs and on the other hand are easy to understand, are still rarely found. Algebraic Petri nets as proposed by Kindler and Reisig allow to concisely model distributed algorithms. Moreover, classical Petri net techniques in combination with a temporal logic can be used to verify the correctness of these models. This paper presents a simple example which provides the flavor of how distributed algorithms can be modeled and verified by help of algebraic Petri nets. Some verification techniques are presented in more detail in separate notes which are interspersed within the text.
Keywords: algebraic Petri nets, algorithm verification, distributed algorithms.