Note: This is an archvied version of our old webpage. Some links might be broken. The current one can be found here.
I7 Logo
Chair for Foundations of Software Reliability and Theoretical Computer Science
Informatik Logo TUM Logo
Petri Nets 2020

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

Material

  • 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: