Representation and execution of Petri nets using rewriting logic as a unifying framework

Mark Oliver Stehr, José Meseguer, Peter Csaba Ölveczky

Research output: Contribution to journalConference articlepeer-review


We give a high-level overview of our recent results which extend and unify the lines of research initiated by Meseguer and Montanari under the motto "Petri nets are monoids", and by Marti-Oliet, Meseguer and other authors in their linear logic axiomization of Petri nets. In particular, we investigate the use of rewriting logic, which was partially inspired by the two aforementioned approaches, as a unifying semantic framework for different Petri net models. To this end, we equip place/transition nets with a rewriting semantics which is sound and complete in the strong categorical sense of a natural isomorphism between the Best-Devillers process semantics and the semantics obtained via rewriting logic. In addition to place/transition nets we consider algebraic net specifications which subsume colored Petri nets and we show how a corresponding sound and complete rewriting semantics can be established at this level. Furthermore, we discuss how rewriting logic can be used to represent other important extensions of the basic Petri net model such as place/transition nets with test arcs and timed Petri nets. Apart from the conceptual unification of different models in a field which has to cope with increasing diversity, this work has interesting practical applications ranging from the execution and analysis of Petri net models, using a rewriting engine such as Maude, to formal verification taking advantage of the logical side rather than the operational side of rewriting logic.

Original languageEnglish (US)
Pages (from-to)140-162
Number of pages23
JournalElectronic Notes in Theoretical Computer Science
Issue number4
StatePublished - Jul 2001
Externally publishedYes
EventUNIGRA 2001, Uniform Approaches to Graphical Process Specification Tehcniques (a Satellite Event of ETAPS 2001) - Genova, Italy
Duration: Mar 31 2001Apr 1 2001

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Representation and execution of Petri nets using rewriting logic as a unifying framework'. Together they form a unique fingerprint.

Cite this