Kiehn: Zeitautomaten

V O R L E S U N G

Zeitautomaten

und andere Modelle für Realzeitsysteme

Vertiefungsvorlesung aus dem Bereich III (Theoretische Informatik) im WS0102




Dozentin: Dr. Astrid Kiehn

Zeit und Ort:

Hörerkreis: Studierende im Hauptstudium der Informatik, Studierende im Hauptstudium mit Nebenfach Informatik
Empfehlenswert bei: Interesse für die Modellierung und Verifikation zeitkritischer Systeme, Automatentheorie


Inhalt:

Das klassische Automatenmodell abstrahiert von der Zeit: der Zustand eines Automaten kann durch das Ausführen einer Aktion unabhängig davon verändert werden, wie lange der bisherige Zustand bereits eingenommen war. Für die Modellierung zeitkritischer Systeme (der Steuerung von chemischen Prozessen beispielsweise) ist solch ein Modell nicht ausreichend. Hierfür sind Konzepte wie Time-Outs, Watch Dogs u.ä. nötig. Zur Modellierung solcher Realzeitsysteme sind in den letzten Jahren viele der bekannten Modelle um Zeitkonzepte erweitert worden.

Der erste Teil der Vorlesung gibt eine Einführung in die Zeitautomaten und darauf aufbauende Verifikationstechniken. Ein Zeitautomat besteht aus einem herkömmlichen Automaten, der mit einer Anzahl von Uhren ausgestattet ist. Sie können abgefragt und gegebenenfalls zurückgesetzt werden. In der Vorlesung behandelt werden Automatenkonstruktionen, unentscheidbare Probleme, die Beziehung zu herkömmlichen Automaten und unterschiedliche Modellierungen der Zeit (diskret über die natürlichen Zahlen oder kontinuierlich über die reellen Zahlen), Verifikationsmöglichkeiten.

Der zweite Teil der Vorlesung zeigt, in welcher Art Petrinetze und Prozeßalgebren, also Modelle für verteilte Systeme, um zeitliche Konzepte erweitert wurden.

Literatur:

Ein den ganzen Stoff der Vorlesung umfassendes Buch gibt es noch nicht. Teile der Vorlesung können aber über das Buch

E. Clarke, O. Grumberg, D. Peled: Model Checking, MIT Press, 2000

vertieft werden. Ein einführender Artikel zu Zeitautomaten ist

R. Alur, T.A. Dill: A theory of timed automata
Theoretical Computer Science, Nr. 126, S.: 183-235, 1994.
(in der Fachbereichsbibliothek einsehbar und kopierbar)

Die Vorlesung baut auf folgenden Arbeiten auf: Literaturliste

Astrid Kiehn