Tuesday June 25
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 led 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 characterized 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.
