Zum Inhalt springen
  • de
  • en
Menü
Technische Universität München
Technische Universität München

Petri Nets (IN2052)

Lecturer (assistant)
Type  
Duration 4 SWS
Language of instruction English

 

Moodle page

You can find the latest information regarding this course at its Moodle page

Dates

Lectures and tutorials

  • Tuesdays: 14:00 to 16:00 (in fact 14:00 to 15:30)
  • Wednesdays: 10:00 to 12:00 (in fact 10:15 to 11:45)

 

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:

  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

 

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

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.

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:

  • 2020 (with solutions)
  • You can find the exams from previous years here.

 

Material

  • Lecture notes: 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:
    • An SMT-based Approach to Coverability Analysis (CAV 2014) [Paper][Slides]
    • An SMT-based Approach to Fair Termination Analysis (FMCAD 2014) [Paper][Slides]
  • 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:
To top