Petri Nets and True Concurrency

Standard

One of the first keynotes I had the pleasure of listening to as a doctoral student was given by Javier Esparza at SPIN/ICGT 2010. As a joint (or rather, parallel) meeting of the model checking and graph transformation communities, his lecture – A False History of True Concurrency – presented the key insights and developments in the history of a research area that was interesting for both: the so-called unfolding approach to model checking.

Unfoldings are a mathematical formalism that give a truly concurrent semantics to a system; that is to say, a partial-order semantics that identifies immaterial orderings of events – orderings that would otherwise be forced in concurrency defined by interleaving. They were interesting for the SPIN community as a means to alleviate state space explosion; interesting too for those at ICGT, with the technique having an analogous use in automatically verifying graph grammars. As a fresh-faced doctoral student, I was fascinated by the theory and applications that the talk examined; although I never got a chance to explore them in my own work.

A Petri net unfolding

A Petri net unfolding

I was delighted however to be able to revisit some of these ideas in the concurrency course that I teach at ETH (jointly with Sebastian Nanz and Bertrand Meyer). The second half of the course has traditionally focused on formal models and process calculi for concurrency, but has never covered the important mathematical modelling language of Petri nets; an omission that this year we addressed. In addition to covering the intuition needed for constructing and interpreting Petri nets, we also used them as a vehicle to compare a semantics based on interleaving and a semantics based on true concurrency, applying the unfolding technique directly to nets and discussing the implications for automatic analysis. Though the lecture is only short, and omits many important details (such as how to search for an appropriate finite prefix), I hope that it still might serve as a useful gentle introduction to Petri nets and true concurrency; hence this post to share it!