Model Checking for Petri Nets
From Algorithms to Technology
In the beginning, model checking was just a set of algorithms: given a system model and a specification (written in a temporal logic), decide whether the model satisfies the specification. The problem is challenging, mainly due to the state explosion problem. State explosion can be addressed in various ways. This has lead to a wealth of technology: data structures, implementations, and approaches. In this course, model checking differentiated by the application domain. For instance, the main challenge in software model checking is to find appropriate abstractions for the data structures.
Petri net model checking has developed into its own branch of model checking. It can be characterised by:
- Absence of data structures (most Petri net model checkers operate on place/transition nets),
- Locality, monotonicity, and linearity of the firing rule,
- Presence of massive concurrency, and
- Availability of results from Petri net theory.
Since 2011, progress in Petri net model checking has been propelled through the yearly Model Checking Contest.
The tutorial spans the whole spectrum from basic algorithms to state-of-the-art technology. At every stage, we show where and how our application domain Petri nets impacts the design of a Petri net model checker. We demonstrate the results using the LoLA 2 model checking tool that is freely available.
Karsten Wolf has his PhD from Humboldt-Universität zu Berlin where he worked with Peter Starke and Wolfgang Reisig. He visited TU Dresden, TU Helsinki, and CMU Pittsburgh. Since 2006, he is a professor at Universität Rostock. Karsten Wolf has contributed several papers on Petri net model checking and is the main developer of the Petri net model checking tool LoLA.
Session 1: Introduction to Model Checking
- Temporal logic LTL
- Temporal logic CTL
- Basic model checking algorithms
Session 2: State space reduction
- Partial order reduction
- Sweep-Line method
Session 3: Basic technology
- Exploiting locality
- Exploiting linear algebra
- Exploiting siphons and traps
Session 4: Advanced technology
- Formula management
- Portfolio approach
- Strength reduction
Earning credit points
For participants who want to earn credit points for the tutorial, we provide a small verification case study that can be executed offline.