In: 4: International Journal of Computer Mathematics, Vol. 31, No. 3, pages 153-165. 1989.
Abstract: Distributed computing systems can be modeled adequately by Petri nets. The computation of invariants of Petri nets becomes necessary for proving the properties of modeled systems. This paper presents a two-phase, bottom-up approach for invariant computation and analysis of Petri nets. In the first phase, a newly defined subnet, called the RP-subnet, with an invariant is chosen. In the second phase, the selected RP-subnet is analyzed. Our methodology is illustrated with the dining philosophers' problem and the connection-disconnection phase of a transport protocol.
Keywords: distributed computing system; net-invariant computation; RP-subnet; dining philosophers' problem; transport protocol.