Process versus unfolding semantics for Place/Transition Petri nets

José Meseguer, Ugo Montanari, Vladimiro Sassone

Research output: Contribution to journalArticle

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.

Original languageEnglish (US)
Pages (from-to)171-210
Number of pages40
JournalTheoretical Computer Science
Volume153
Issue number1-2
DOIs
StatePublished - Jan 8 1996
Externally publishedYes

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Process versus unfolding semantics for Place/Transition Petri nets'. Together they form a unique fingerprint.

  • Cite this