Temporale Logik und Zustandssysteme (PG)

Aktuelles

15.11.99: Auf den Linux-Rechnern am CIP-Pool ist das Entscheidungsverfahren ptl für lineare temporale Aussagenlogik installiert. (Das Programm sollte im Pfad sein, notfalls explizite Pfadangabe /soft/IFI/sci/ptl/iX86-unknown-linux/bin/ptl.) Beispiele dazu liegen im Verzeichnis /soft/IFI/sci/ptl/share/ex/. Weitere Details auf der Manpage (man ptl). Bei Problemen bitte email.

Inhalt

Temporale Logik ist eine Erweiterung der klassischen mathematischen Logik, bei der Aussagen in verschiedenen Zuständen (Zeitpunkten) verschiedene Wahrheitswerte haben können. Sie eignet sich somit als logische Grundlage zur formalen Behandlung von Zustandssystemen.

Die Vorlesung gibt eine ausführliche Einführung in verschiedene Varianten dieser Logik (hauptsächlich lineare und verzweigte Temporallogik sowie TLA) und entwickelt systematisch ihre Anwendungsmöglichkeiten im Bereich der Spezifikation und Verifikation (einschließlich model checking) von Systemen. Als spezielle Anwendung wird die Verifikation paralleler Programme behandelt.

Während der Vorlesung wird ausführliches Begleitmaterial ausgegeben. Die Vorlesung beginnt in der ersten, die Übungen in der zweiten Woche.

Personen

Termine

Dienstag    11-13 Uhr    Vorlesung   Raum  1.35, Oettingenstr.67  BEGINN 2.11.
Donnerstag  14-16 Uhr    Vorlesung   Raum  1.35, Oettingenstr.67
Mittwoch     9-11 Uhr    Übung       Raum  0.33, Oettingenstr.67  BEGINN 10.11.

Literatur

• D. Gabbay, I. Hodkinson, M. Reynolds: Temporal Logic - Mathematical Foundations and Computational Aspects. Vol. 1. Oxford: Clarendon Press, 1994
• F. Kröger: Temporal Logic of Programs. EATCS Monographs on Theoretical Computer Science, vol. 8. Berlin: Springer-Verlag, 1987
• Z. Manna, A. Pnueli: The Temporal Logic of Reactive and Concurrent Systems. Vol.1: Specification. New York: Springer-Verlag, 1992

Übungsbetrieb

Die Übungsblätter werden in der Vorlesung am Donnerstag verteilt. Die Aufgaben werden am Mittwoch der Folgewoche in der Übung besprochen. Die Hausaufgaben sollen in der Übung abgegeben werden. Sie werden dann eine Woche später korrigert zurückgegeben. Die Hausaufgaben, die mit einer Punktezahl gekennzeichnet sind, sind relevant fuer die Zulassung zur Klausur und sollten deshalb in jedem Fall abgeben werden.

Die erste Übung findet am Mittwoch, den 10.11.1999 statt.

Klausur und Schein

Voraussetzung zum Erwerb des Übungsscheins sind 50% der mit Punkten versehenen Hausaufgaben sowie das Bestehen der Klausur bzw. einer mündlichen Prüfung.

Zur Vorbereitung ist hier die Klausur zur Vorlesung im Wintersemester 1997/98 verfügbar (DVI oder Postscript). Man sollte auf jeden Fall versuchen, die Aufgaben selbst zu lösen und erst dann die Lösungsvorschläge (DVI oder Postscript) vergleichen. (Nicht erschrecken! Die Klausur war etwas zu kompliziert und zu lang.)