Petri Nets (IN2052)
Lecturer | |
---|---|
Assistant | Guttenberg Roland |
Duration | 4 SWS |
Language of instruction | English |
Moodle page
You can find the exercise sheets and lecture notes at the Moodle page of the lecture.
Dates
Lectures and tutorials
- Wednesdays: 10:15 to 11:45
- Fridays: 12:00 to 13:30
In general, we try to stick to the schedule of having three lectures following by one tutorial, i.e. a tutorial on every second friday. The planned dates for tutorials are:
- Friday 26. April: 12:00 to 13:30
- Friday 10. May: 12:00 to 13:30
- Friday 24. May: 12:00 to 13:30
- Friday 7. June: 12:00 to 13:30
- Friday 21. June: 14:15 to 15:45
- Friday 28. June: 12:00 to 14:00 (observe the 1-week gap)
- Friday 12. July: 12:00 to 14:00
Content
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:
- Reachability and coverability graphs.
- Techniques based on well-quasi-orders.
- Place and transition invariants, siphons and traps
- Structure theory: Marked Graphs and Free Choice nets
- Petri net unfoldings
Exercises
Exercises are voluntary and do not account for the final grades. It is highly recommended to work on the exercises, as this is the best preparation for the exam.
Past exercise sheets
Summer 2020
- Exercise sheet 1
- Exercise sheet 2
- Exercise sheet 3
- Exercise sheet 4
- Exercise sheet 5
- Exercise sheet 6
- Exercise sheet 7
- Exercise sheet 8
Previous years
You can find the exercise sheets for the previous years here.
Exam
The final grade is determined by a written exam at the end of the term. The dates for the exam are:
- Endterm: 1. August 2024
- Retake: 30. September 2024
To prepare yourself for the exam, you are strongly encouraged to take some past exams at home. It is additionally encouraged to go through the exercise sheets.
Past exams:
Old Material (Current material on moodle page)
- Lecture notes of SS2022: here
- Notes from SS 2016:
- This set of slides introduces some basic definitions:
- Place, transition, arc, token, marking, firing rule.
- Causality, conflict, concurrency.
- Deadlock-freeness, liveness, boundedness
- Papers on checking coverability and fair termination of Petri nets with an SMT solver:
- In the last part of the course I'll use material from these books: Notice that you can download them directly (for free) through the links above.
- This paper by Prof. Tadao Murata was published in 1989, but it still is a very nice introduction to Petri nets. The paper has over 12000 citations in Google Scholar!
- The Petri Nets World is a very interesting site with lots of information on all aspects of Petri nets. In particular you can find there a list of Petri net tools.
- There are many tools for editing and analyzing Petri nets.
- A reasonable tool, very easy to install, although with some annoying bugs, is PIPE2 (Platform Independent Petri net Editor 2). It is best to download version 4 from SourceForge, as version 5 (on GitHub) has removed some analysis features.
- CPNTools is a very sophisticated, more professionally developed, tool for coloured Petri nets. It is also very easy to install, but more difficult to understand!
- APT is command-line based Java tool with many functions for analyzing Petri nets, such as checking boundedness or liveness, finding traps, siphons and invariants and constructing reachability and coverability graphs.
- LoLA is a command-line based tool written in C++ which can answer queries on Petri nets such as reachability or deadlock checking.
- In SS13 I used my laptop as a blackboard, and I put the resulting handwritten notes online.
Just in case you find them useful, here are the handwritten notes of SS13:- Backwards coverability algorithm:
- Abstract backwards reachability algorithm.
- The marking equation
- Place and transition invariants
- Structure theory