materials
material download
activity confirmation
exam criteria Seminar: Theoretical Foundations of Model Checking - winter term 06/07
material
ILIAS
| LaTeX slides example | zipped LaTeX template | |
| LaTeX LNCS example | zipped LaTeX template | |
| LaTeX LNCS style | zipped LaTeX style | |
Slides
Topics
| 01. Büchi automata and logics | techincal report | |
| 02. Deciding Presburger arithmetic using automata | conference publication | |
| 03. Deciding linear arithmetic using automata | conference publication | |
| 04. Automata and don't care words | conference publication | |
| 05. Hybrid automata | conference publication | |
| 06. model checking hybrid automata using polyhedra | journal, conference publication | |
| 07. Reachability analysis of hybrid automata | conference publication | |
| 08. Model checking hybrid automata using predicate abstractions | journal | |
| 09. Model checking using automata abstractions | conference publication | |
| 10. Bisimilarity and characterization of Kripke-structures | journal | |
| 11. Branching bisimulation and its characterization | journal, conference publication | |
Written elaborations
| 02. Deciding Presburger arithmetic using automata | ||
| 03. Deciding linear arithmetic using automata | ||
| 04. Automata and don't care words | ||
| 05. Hybrid automata | ||
| 06. model checking hybrid automata using polyhedra | ||
| 07. Reachability analysis of hybrid automata | ||
| 10. Bisimilarity and characterization of Kripke-structures | ||
| 11. Branching bisimulation and its characterization | ||