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 SS04




Dozentin: Dr. Astrid Kiehn

Zeit und Ort: donnerstags 8.30 -10.00, Raum 00.09.022

Beginn: 22.04.04

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


Inhalt:

Die Vorlesung gibt einen Einblick in die Spezifikations- und Verifikationsmöglichkeiten zeitkritischer Systeme insbesondere am Beispiel von Zeitautomaten.

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 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. Die Vorlesung gibt eine Einführung in die Theorie der Zeitautomaten. 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ülichen Zahlen oder kontinuierlich über die reellen Zahlen) und darauf aufbauende Verifikationsmöglichkeiten. Es wird auf neuere Forschungsarbeiten eingegangen.

Soweit noch Zeit verbleibt, wird im zweiten Teil der Vorlesung gezeigt, in welcher Art Petrinetze und Prozeßalgebren um zeitliche Konzepte erweitert wurden.

Skript: gibt es keines, die Folien aus der Vorlesung werden aber an dieser Stelle zur Verfügung gestellt.

Folien aus der Vorlesung

Literatur:

Der grundlegende und sehr gut lesbare 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)

Teile der Vorlesung können über das Buch

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

vertieft werden.

Literaturliste

Astrid Kiehn