mctextbook
Talks on Model-Checking Book
In these talks the students present the chapters of the Baier-Katoen “Principle of Model Checking” book and Manna-Pnueli “The temporal logic of reactive and concurrent systems” book Back to Start page
| Title | Slides |
|---|---|
| Regular properties, part I: regular safety properties | slides |
| Regular properties, part II: ω-regular properties | slides |
| Regular properties: part III: model checking with Büchi automata | slides |
| Linear Temporal Logic (LTL), part I: syntax and semantics of LTL | slides |
| Linear Temporal Logic (LTL), part II: automata-based LTL model checking | slides |
| Linear Temporal Logic (LTL), part III: complexity of LTL model checking | slides |
| Computation Tree Logic (CTL), part I: syntax and semantics of CTL | slides |
| Computation Tree Logic (CTL), part II: expressiveness of CTL and LTL | slides |
| Computation Tree Logic (CTL), part III: CTL model checking | slides |
| Computation Tree Logic (CTL), part IV: CTL with fairness | slides |
| Computation Tree Logic (CTL), part V: CTL+ and CTL* | slides |
mctextbook.txt · Last modified: 2017/04/18 10:32 by 127.0.0.1