In: Rozenberg, G.: Lecture Notes in Computer Science, Vol. 609; Advances in Petri Nets 1992, pages 21-69. Springer-Verlag, 1992.
Abstract: A new Petri net calculus called the calculus of Petri Boxes is described. It has been designed to allow reasoning about the structure of a net and about the relationship between nets, and to facilitate the compositional semantic translation of high level constructs such as blocks, variables and atomic actions into elementary Petri nets. The calculus is located `midway' in such a translation. This paper first defines an algebra of Box expressions. A corresponding algebra of Boxes is then defined and used compositionally as a semantic model of Box expressions. The two algebras feature a general asynchronous communication operation extending that of CCS. Synchronization is defined as a unary operator. The algebras also include refinement, iteration and recursion. It is shown how they can be used to describe data and blocks. As the main results of this paper, it is proved that the Box algebra satisfies various desirable structural laws and enjoys two important behavioral properties. The paper also contains an example proof of a mutual exclusion protocol.
Keywords: Petri Nets; Process Algebras; Compositional Semantics; Multiway Synchronization; Refinement; Recursion; Data.