Petri Nets 2020

News | Content | Dates | Grading | Material | Exercises | Exam | Contact

Petri nets are a formal model for concurrent systems invented in the 1960s by Carl Adam Petri. Petri nets combine a simple, clear graphical notation with a precise semantics, and a wealth of available techniques for analysis and verification. The structure of Petri nets intuitively visualizes fundamental concepts of concurrency such as causality and conflict.

Petri nets provide a formal semantics for several industry standards like UML activity diagrams (a notation for the representation of workflows), or BPNM and EPCs, two languages for the description of business processes. They are also directly used to model and analyze manufacturing systems, communication protocols, hardware designs, business processes, and biological sytems. The Petri net group at Aarhus University in Denmark maintains this web page with many case studies.

The course teaches the fundamentals of the theory of Petri nets. (This is a theory course!) It introduces several variants of Petri nets, but focuses on the most popular model, place-transition Petri nets. The course introduces the main techniques for analyzing and verifying properties of Petri nets:

1. Reachability and coverability graphs.
2. Techniques based on well-quasi-orders.
3. Place and transition invariants, siphons and traps
4. Structure theory: Marked Graphs and Free Choice nets
5. Petri net unfoldings