Model-Checking SS 2018

Exercise Sheets

• 1. Introduction
  Exercise sheet: [PDF]
  Some useful links: Spin README Spin references Modex
• 2. Linear temporal logic (LTL)
  Exercise sheet: [PDF] | [Solutions]
  Extra sheet on LTL equivalences: [PDF] | [Solutions]
  Spot is available at https://spot.lrde.epita.fr. In particular, the on-line translator used in class is here, and you can obtain sequences satisfying a formula through the "Büchi Run" panel.
• 3. Promela and Spin
  Exercise sheet: [PDF] | [Tips] | [Solution 3.1.1, 3.1.2] | [Solution 3.1.4]
  Solution to Exercise 3.2 would be uploaded at a later date
• 4. Büchi automata
  Exercise sheet: [PDF] | [Solutions]
• 5. LTL to Büchi automata translation
  Exercise sheet: [PDF]
• 6. Emptiness check
  Exercise sheet: [PDF] | [Solutions]
• 7. Partial-order reduction
  Exercise sheet: [PDF] | [Solutions]
• 8. Computation tree logic (CTL)
  Exercise sheet: [PDF] | [Solutions]
• 9. Binary decision diagrams (BDD)
  Exercise sheet: [PDF]
• 10. NuSMV and CTL
  Exercise sheet: [PDF] | [Solutions]
  SMV files: [Ex. 10.1] | [Ex. 10.2]
• 11. Abstraction, simulation and bisimulation
  Exercise sheet: [PDF] | [Solutions]
• 12. Pushdown systems
  Exercise sheet: [PDF] | [Solutions]
  Python script to compute Pre*: pre_star.py