| Literatur |
Modeling and Analysis of Hybrid Systems, Lecture Notes by Prof. Dr. Erika Abraham, RWTH Aachen University
On Reachability for Hybrid Automata over Bounded Time, T. Brihaye, L. Doyen, G. Geeraerts, J. Ouaknine, J.-F. Raskin, and J. Worrell
Parts fo Chapter 9 of Principles of Model Checking, Christel Baier and Joost-Pieter Katoen, MIT Press
A tutorial on UPPAAL. G. Berhmann and A. David and K.G. Larsen, Springer
The material will be made available through Learnweb. |
| Bemerkung |
Für Studierende des MEd GymGes Informatik (nach LABG 2009): Wenn Sie diese Vorlesung für das Vertiefungsmodul I belegen möchten, dann müssen Sie auch die zugehörigen Übungen (HISLSF-Link: hier) absolvieren.
Studierende in den alten Studiengängen müssen in den Wahlbereichen bzw. in den Modulen Praktische Informatik und Spezialisierung ebenfalls die zugehörigen Übungen absolvieren, ebenso Studierende im M.Ed. Gym/Ges Informatik im Modellversuch. |
| Lerninhalte |
Die Vorlesung führt in die Theorie der Hybriden Systeme aus Sicht der Informatik ein. Wir erweitern einfache Zustandstransitionssysteme um Zeit und erhalten sogenannte Zeitautomaten. Weiterhin betrachten Timed Temporal Logics und erarbeiten TCTL model checking für Zeitautomaten. Nach einer Fallstudie mit dem Tool UPPAAL, lernen wir verschiedene Varianten von Hybriden Automaten kennen. Von Rechteckautomaten, über lineare hybride Automaten arbeiten wir uns an allgemeine Hybride Automaten heran, betrachten Entscheidbarkeitsresultate und lernen Abstraktionsverfahen zur Lösung von Erreichbarkeitsproblemen kennen. Zum Abschluss gibt die Vorlesung einen Einblick in aktuelle Forschung auf dem Gebiet von Hybriden Petri Netzen und stellt deren Transformation in Hybride Automaten sowie eine stochastische Erweiterung vor. |
eG