Inhalt
In diesem Seminar werden Systeme behandelt, deren Verhalten nicht nur durch die Veränderung diskreter Zustände, sondern auch kontinuierlicher Parameter bestimmt ist. Hierzu gehören Parameter wie die linear fortschreitende Zeit („timed systems“) oder Größen wie Temperatur, die z.B. durch Differentialgleichungen beschrieben werden („hybrid systems“).
Es wird zum einen die Modellierung derartiger Systeme betrachtet, zum anderen aktuelle Ansätze zur algorithmischen Verifikation und Synthese, insbesondere in Hinblick auf deren Anwendungspotential. Themen sind u.a.:
Hybride Systeme und Zeit-Automaten
Model-Checking
Simulation
Algorithmische Synthese (Spieltheorie, Supervisory Control Theory)
Themen
The Theory of Timed Automata
The Theory of Hybrid Automata
Real-Time Model Checking
Model-Checking of Hybrid Systems
The Theory of Controller Synthesis (Game Theory & Supervisory Control Theory)
Controller Synthesis under real-time constraints
Synthesis of Hybrid Control Systems
Modeling and Model-Checking using Hybrid Automata: Case Study „Electronic Height Control“
Abstraction-Based Controller Synthesis using Hybrid Automata: Case Study „Chemical Process Control“
Model-Checking Embedded Systems Assembly Code
Ablauf
Dieses Seminar wird als Blockseminar durchgeführt. Das erste Treffen wird am Ende der vorlesungsfreien Zeit oder zum Beginn des Wintersemesters durchgeführt. Das Blockseminar wird dann im Februar 2008 an zwei aufeinander folgenden Tagen abgehalten. Zwischendurch wird es einige Deadlines zur Abgabe der schriftlichen Ausarbeitung und der Folien geben, die eingehalten werden müssen.
Termine
Anforderungen
Teilnahme an allen Terminen
Eigenständige Einarbeitung in das gegebene Thema
Schriftliche Ausarbeitung von 10-15 Seiten / Person in der von uns zur Verfügung gestellten Vorlage
Vortrag von 30 Minuten (strikt) / Person
Deadlines strikt (Es genügt die Dateien per E-Mail zu schicken. Kein Schein bei zweimaligem Verpassen der Deadlines!):
10.11.07: zusätzliche Literatur
30.11.07: Gliederung und kurze Inhaltsangabe zu jedem Abschnitt
10.01.08: schriftliche Ausarbeitung & Folien
Die Ausarbeitung und die Folien müssen selbstständig verfasst werden. Alle benutzten Quellen und Hilfsmittel müssen angegeben sowie Zitate kenntlich gemacht werden.
Unterlagen
Kontakt