| Proseminar | Literatur-Links | Folien und Ausarbeitungen |
The Time Machine
 |
Proseminar im Sommersemester 2006 9/5 Leistungspunkte Kolloquium: 8./9. August, 9 Uhr Gebäude E1 1, Raum 407 Bernd Finkbeiner Klaus Dräger Hans-Jörg Peter Vorbesprechungsfolien und Themenzuordnung |
Wie modelliert man Zeit?
Gezeitete Systeme beinhalten außer der diskreten Struktur auch eine zeitliche Komponente. Hierzu werden Standardmodelle wie endliche Automaten um Uhren, die den Verlauf der Zeit beschreiben, erweitert. Das einfachste derartige Modell sind Timed Automata; wir werden im Rahmen des Proseminars dieses und andere Modelle (z.B. Timed Petri Nets, Hybrid Automata) kennenlernen.
Welche Eigenschaften sind entscheidbar?
Gezeitete Systeme haben einen unendlichen Zustandsraum, daher ist es nicht offensichtlich, wie ihr Verhalten beschrieben werden kann. Erst durch geeignete Abstraktionen des Zustandraums lassen sich diverse Probleme lösen. Zu diesen Problemen zählen Model Checking (Verifikation von temporallogischen Aussagen) oder Synthese (automatische Erzeugung eines Systems aus einer Spezifikation).
Wie gewinnt man ein Spiel gegen die Zeit?
In manchen Szenarien muss ein System mit einer Umgebung (z.B. anderen Prozessen) interagieren, die nicht kontrollierbar ist. Solche Fragestellungen lassen sich als gezeitete Spiele modellieren. Das Finden einer Gewinnstrategie für gezeitete Spiele ist zum Beispiel ein zentrales Problem bei der Synthese von Controllern.
Darf Zeit stehen bleiben?
Bei einem Wettlauf gibt Achilles einer Schildkröte genau einen Meter Vorsprung. Wenn er den Startpunkt der Schildkröte erreicht, dann ist sie bereits 1/k Meter weitergelaufen. Wenn Achilles diese 1/k Meter aufgeholt hat, ist die Schildkröte schon wieder 1/k² Meter entfernt… Holt Achilles die Schildkröte jemals ein?