In: Dassow, J.; et al.: Lecture Notes in Computer Science, Vol. 464; Aspects and Prospects of Theoretical Computer Science. Proceedings of the 6th International Meeting of Young Computer Scientists (IMYCS), 1990, Smolenice, Czechoslovakia, pages 159-168. Berlin, Germany: Springer-Verlag, 1990.
Abstract: A network of processes exchanging information by message passing is called a distributed system. Each process has computing and storage facilities and is connected to some other processes via bidirectional communication channels. Termination detection in such a distributed system is one of the classical theoretical problems. To verify a solution for this problem correctly a formal model must be chosen. The solution presented in this paper is based on Petri nets with structured tokens. For formal verification, in particular place invariants are used, and graph-theoretical concepts are integrated into the calculus by regarding some predicates in the set of reachable markings.
Keywords: distributed termination problem; bidirectional communication channel; structured tokens; place invariants; reachable marking.