I7 Logo
Chair for Foundations of Software Reliability and Theoretical Computer Science
Informatik Logo TUM Logo
Model-Checking SS 2018

  News | Basic information | Content | Exercises | Slides | Links | Exam

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