Model-Checking SS 2017

Exercise Sheets

• Exercise sheet #1 [PDF] Some useful links: Spin README Spin references Modex
• Exercise sheet #2 [PDF] [Solution] On LTL
• Exercise sheet #3 [PDF] [Solution 3.1 (1-3), Solution 3.1 (4-5), Solution 3.2] On Promela and Spin
• Exercise sheet #4 [PDF] [Solution] More on LTL and Büchi automata
• Exercise sheet #5 [PDF] [Solution] LTL to Büchi automata translation
• Exercise sheet #6 [PDF] [Solution] Emptiness check
• Exercise sheet #7 [PDF] [Solution] Partial-order reduction
• Exercise sheet #8 [PDF] [Solution] CTL
• Exercise sheet #9 [PDF] [Solution] NuSMV
• Exercise sheet #10 [PDF] [Solution] BDDs
• Exercise sheet #11 [PDF] [Solution] Abstraction, simulation and bisimulation
• Exercise sheet #12-13 [PDF] Abstraction refinement, pushdown systems