|
|
|
|
|
|
|
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:
- Backwards coverability algorithm:
- Abstract backwards reachability algorithm.
- The marking equation
- Place and transition invariants
- Structure theory
|
|
|
|
|
|
|