Weekly Notes for Week 26

This week we will still work on Petri nets. We will continue with modelling and model-checking questions, and we will discuss why even restricted Petri-net reachability questions can become computationally hard.

There is no new slide deck for this week. We will continue to use the Petri net slides from the previous weeks, in particular the material on reachability, coverability, invariants, Farkas’ algorithm, and complexity.

• Slides and reading:

  • Petri-net slides
  • Petri-net invariants and Farkas’ algorithm
  • Esparza, Decidability and Complexity of Petri Net Problems
  • Murata, Petri Nets: Properties, Analysis and Applications

• Exercises:

  • Continue with the updated Exercise Sheet 07: Petri Nets – Modelling and Model Checking
  • The sheet now also contains a theoretical exercise on NP-completeness of acyclic 1-safe place reachability.
  • LoLA command-line material: README and example files