Technical reports

Petri net semantics

Jonathan M. Hayman

June 2010, 252 pages

This technical report is based on a dissertation submitted January 2009 by the author for the degree of Doctor of Philosophy to the University of Cambridge, Darwin College.

DOI: 10.48456/tr-782

Abstract

Petri nets are a widely-used model for concurrency. By modelling the effect of events on local components of state, they reveal how the events of a process interact with each other, and whether they can occur independently of each other by operating on disjoint regions of state.

Despite their popularity, we are lacking systematic syntax-driven techniques for defining the semantics of programming languages inside Petri nets in an analogous way that Plotkin’s Structural Operational Semantics defines a transition system semantics. The first part of this thesis studies a generally-applicable framework for the definition of the net semantics of a programming language.

The net semantics is used to study concurrent separation logic, a Hoare-style logic used to prove partial correctness of pointer-manipulating concurrent programs. At the core of the logic is the notion of separation of ownership of state, allowing us to infer that proven parallel processes operate on the disjoint regions of the state that they are seen to own. In this thesis, a notion of validity of the judgements capturing the subtle notion of ownership is given and soundness of the logic with respect to this model is shown. The model is then used to study the independence of processes arising from the separation of ownership. Following from this, a form of refinement is given which is capable of changing the granularity assumed of the program’s atomic actions.

Amongst the many different models for concurrency, there are several forms of Petri net. Category theory has been used in the past to establish connections between them via adjunctions, often coreflections, yielding common constructions across the models and relating concepts such as bisimulation. The most general forms of Petri net have, however, fallen outside this framework. Essentially, this is due to the most general forms of net having an implicit symmetry in their behaviour that other forms of net cannot directly represent.

The final part of this thesis shows how an abstract framework for defining symmetry in models can be applied to obtain categories of Petri net with symmetry. This is shown to recover, up to symmetry, the universal characterization of unfolding operations on general Petri nets, allowing coreflections up to symmetry between the category of general Petri nets and other categories of net.

Full text

PDF (2.1 MB)

BibTeX record

@TechReport{UCAM-CL-TR-782,
  author =	 {Hayman, Jonathan M.},
  title = 	 {{Petri net semantics}},
  year = 	 2010,
  month = 	 jun,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-782.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-782},
  number = 	 {UCAM-CL-TR-782}
}