Compositional reification of petri nets

Abstract

A categorical semantic domain is constructed for the reification of Petri nets based on graph transformations. First, the graph transformation concept (based on the single pushout approach) is extended for Petri nets viewed as graphs with partia! morphisms. Classes of transformations stand for reifications where part of a net (usually a transition) is replaced by another (possible complex) net allowing a hierarchical specification methodology. The composition of reifications (i.e., composition of pushouts) is defined, leading to a category of nets and reifications which is complete and cocomplete. Since the reification operation composes, the vertical compositionality requirement of Petri nets is achieved. Then , it is proven that the reification also satisfies the horizontal compositionality requirement, i.e ., the reification of nets distributes through parallel composition. Techniques for specification of nets, top down design of nets anda notion of bisimulation between unreified and reified net are provided.