In: Rozenberg, G.: Lecture Notes in Computer Science, Vol. 674; Advances in Petri Nets 1993, pages 406-426. Springer-Verlag, 1993.
Abstract: In this paper, we define deterministic systems of sequential processes (DSSP), a class of Petri nets which generalizes the one introduced by Wolfgang Reisig in 1979. In studying this class of Petri nets, we have two aims. Our first aim is to give efficient and formal methods for the validation of a class of systems of sequential processes cooperating by message passing and resource sharing. Our second aim is to show that the modular structure of DSSPs allows us to fully use compositions of nets in the specification and the validation steps of the parallel applications that we describe through DSSPs. Indeed, we give several rules for building in a bottom-up and modular way, a live DSSP. We also give for DSSPs an inexpensive method of liveness validation. Finally, we show that the liveness of a DSSP is monotonic, and that the minimal resources configurations ensuring the liveness are computable. This work is a contribution to the approach which involves developing classes of structured nets in order to specify and validate systems in a modular way via compositions and refinements.