Programming and Computer Software, 2001, Vol.27, No.6, pp.309-319. ISSN: 0361-7688.

Abstract

In the paper, a formal model based on Petri nets is proposed in the context of a compositional approach to the development and analysis of complex concurrent and distributed systems. Mutlilabels of Petri nets are introduced allowing labeling a transition not only with a single symbol, but also with a multiset of symbols. Operations over multilabeled Petri nets---parallel composition and restriction---are defined. A definition of a Petri net entity is given based on the notion of multilabels. A Petri net entity is a Petri net with a set of multilabels where each multilabel is regarded as an access point of the entity. The operation of entity composition is introduced. Equivalence of entities is defined based on bisimulation equivalence of Petri nets. It is shown that the equivalence relation is congruent with respect to entity composition. It is also demonstrated that the composition operation is commutative and associative.

Key words: concurrent systems, distributed systems, Petri nets, Petri net entity, compositionality.