====== Talks on Model-Checking Book ======
In these talks the students present the chapters of the Baier-Katoen "Principle of Model Checking" {{:books:baier-katoen.pdf|book}}
and Manna-Pnueli "The temporal logic of reactive and concurrent systems" {{:books:manna-pnueli.pdf|book}}
[[start|Back to Start page]]
----

^Title ^ Slides ^
|Regular properties, part I: regular safety properties	|{{:Slides:lec08.pdf|slides}}|
|Regular properties, part II: ω-regular properties	|{{:Slides:lec09_10.pdf|slides}}|
|Regular properties: part III: model checking with Büchi automata	|{{:Slides:lec11.pdf|slides}}|
|Linear Temporal Logic (LTL), part I: syntax and semantics of LTL	|{{:Slides:lec12_13.pdf|slides}}|
|Linear Temporal Logic (LTL), part II: automata-based LTL model checking	|{{:Slides:lec14_15.pdf|slides}}|
|Linear Temporal Logic (LTL), part III: complexity of LTL model checking	|{{:Slides:lec15.pdf|slides}}|
|Computation Tree Logic (CTL), part I: syntax and semantics of CTL	|{{:Slides:lec17.pdf|slides}}|
|Computation Tree Logic (CTL), part II: expressiveness of CTL and LTL	|{{:Slides:lec18.pdf|slides}}|
|Computation Tree Logic (CTL), part III: CTL model checking	|{{:Slides:lec19.pdf|slides}}|
|Computation Tree Logic (CTL), part IV: CTL with fairness	|{{:Slides:lec20.pdf|slides}}|
|Computation Tree Logic (CTL), part V: CTL+ and CTL*	|{{:Slides:lec21_01.pdf|slides}}|