In the last few years, the semantics of Petri nets has been investigated in several different ways. Apart from the classical ''token game'', one can model the behaviour of Petri nets via nonsequential processes, via unfolding constructions, which provide formal relationships between nets and domains, and via algebraic models, which view Petri nets as essentially algebraic theories whose models are monoidal categories. In this paper we show that these three points of view can be reconciled. In our formal development a relevant role is played by DecOcc, a category of occurrence nets appropriately decorated to take into account the history of tokens, The structure of decorated occurrence nets at the same time provides natural unfoldings for Place/Transition (PT) nets and suggests a new notion of processes, the decorated processes, which induce on Petri nets the same semantics as that of unfolding. In addition, we prove that the decorated processes of a net can be axiomatized as the arrows of a symmetric monoidal category which, therefore, provides the aforesaid unification.
Process versus unfolding semantics for place/transition Petri nets
MONTANARI, UGO GIOVANNI ERASMO;
1996-01-01
Abstract
In the last few years, the semantics of Petri nets has been investigated in several different ways. Apart from the classical ''token game'', one can model the behaviour of Petri nets via nonsequential processes, via unfolding constructions, which provide formal relationships between nets and domains, and via algebraic models, which view Petri nets as essentially algebraic theories whose models are monoidal categories. In this paper we show that these three points of view can be reconciled. In our formal development a relevant role is played by DecOcc, a category of occurrence nets appropriately decorated to take into account the history of tokens, The structure of decorated occurrence nets at the same time provides natural unfoldings for Place/Transition (PT) nets and suggests a new notion of processes, the decorated processes, which induce on Petri nets the same semantics as that of unfolding. In addition, we prove that the decorated processes of a net can be axiomatized as the arrows of a symmetric monoidal category which, therefore, provides the aforesaid unification.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
