1. What?
2. To Whom?
3. Implementation
4. Contents


Points
Exercises
Reading material
The ASSET model checker
MathCheck minicourse on writing predicates
Other MathCheck exercises
MathCheck parser manuscript


MAT-74506 In Curriculum Book
TCS Studies
Computer-Aided Verification Award 2014

MAT-74506 Model Checking and Petri Nets

Autumn 2016

Updated 2016-11-16

Some exercises have been added to the Exercises document. Some links to block splitting algorithms have been added to the List of reading material.

Two ASSET exercises have been added to the Exercises document. For 2016-09-16, please solve exercise 17 as far as you can. We will discuss your incomplete solutions. Then, for 2016-09-20, complete the solution of exercise 17.

A link to the MathCheck parser manuscript has been added to the right.

Two links to MathCheck exercises have been added to the right.

The course starts on Tuesday, 2016-08-30 at 12:15, in classroom TD 308.

1. What?

Model checking means the use of automated mathematical methods for checking a design of a software or hardware system against errors. Model checking has been successfully used to find bugs that are too rare to be found in testing, but frequent enough to be dangerous. This course covers the general issues in model checking, introduces the most important approaches to model checking, and discusses some techniques in detail.

Petri nets are a mathematical formalism for representing concurrent systems, that is, systems that consist of co-operating components: program threads, hardware units, a mobile phone and the network, …. Thanks to their intuitive graphical representation, Petri nets are well-suited to studying concurrency. Being computationally strictly between finite automata and general computers, they offer interesting algorithmical advantages (at the cost of modelling disadvantages). This course focuses on those aspects of Petri nets that are relevant for model checking.

Pedagocically, the goal of the course is less in the listed topics themselves, and more in learning how theoretical computer science can be used to solve practical problems. The timing of the course is flexible. If necessary, some time will be devoted to background topics in algorithms, theoretical computer science, and logic, to help students with moderate background.

On the other hand, the most advanced topics in the course are directly linked to international top-level research. For instance, we won the 2014 Computer-Aided Verification award and 2012 Petri net outsanding paper award. So this course has something to offer also to ambitious students.

2. To Whom?

The course is intended for both finnish and international students interested in advanced programming issues, theoretical computer science, or discrete mathematics.

If you know how graphs are represented in programs and how depth-first search works, then your background in programming is probably sufficient. Basic notation from set theory and especially logic suffices for background in mathematics. No background in theoretical computer science is assumed.

That is, you need not know much theory now to take the course. However, please be aware that you must learn the theory taught during the course to pass the course. If your plan is to concentrate on the practical side of the course and skip the theory taught in the course, then this course is not for you.

Attitude is more important than background. If your background is weaker than mentioned above, but you are ready to solve extra personal exercises designed for you, then you are welcome to the course. The deal is: I will do my best to adapt the course to your background, and you will do your best to learn during the course.

3. Implementation

The course is on periods 1 and 2. Every week there are three meetings of two hours each. The meetings are flexibly used for lectures, exercises, and discussion. The meetings are on

An assignmnent consists of one or more exercises. You are expected to solve them at home and present the solutions in a meeting. In addition to traditional mathematical, programming, or algorithm design tasks, an exercise may also ask you to find information on some topic and prepare a talk on it. There will also be hands-on model checking exercises using a simple model checker called ASSET.

I plan to design personal assignments adapted to your background and performance. A typical assignment consists of one medium-sized or big exercise, or many small exercises. If an assignment is exceptionally big, then some other assignment to the same student will be exceptionally small, to balance the average workload.

There will be two alternative ways to do the course.

Information on reading material will be provided later. All material will be distributed via this web page or emailed to you.

The teacher of the course is Antti Valmari.

4. Contents

This list of topics is initial and may change.

  1. Petri nets
    • informal introduction via graphical representation
    • definition of place/transition nets
    • enabled transitions and firing of transitions
    • other classes of Petri nets
  2. Behaviour of Petri nets
    • reachability set and reachability graph
    • boundedness
    • some liveness concepts
    • strong components of the reachability graph
  3. Checking simple properties from the reachability graph
    • deadlocks and termination
    • bad states
    • non-progress cycles
    • Büchi acceptance
  4. State explosion
    • the problem
    • on-the-fly verification
    • bit-state hashing
    • exploiting symmetry
    • exploiting parallel hardware
  5. A quick look on invariants and structure theory
    • place invariants
    • transition invariants
    • traps and siphons
    • free-choice nets
  6. Temporal logics
    • Linear-time Temporal Logic
    • safety, liveness and fairness
    • Computation Tree Logic (branching time)
    • Computation Tree Logic Star
  7. Model-checking temporal logics
    • basic CTL verification algorithm
    • translation of LTL to Büchi automata
    • computational complexity
  8. Stubborn sets (partial-order verification)
    • deadlock-preserving method
    • construction of stubborn sets
    • verifying safety properties
    • verifying linear-time properties
    • verifying branching-time properties
  9. Binary decision diagrams
    • definition
    • verification algorithms
    • complexity considerations
  10. Bounded model checking
    • SAT solvers
    • translation to SAT
    • more general solvers
  11. Coverability sets
    • mathematics
    • modern algorithm
  12. Conclusion