Temporale Logik

Aktuelles

22.1.99: Auf Übungsblatt 10 hat sich ein Druckfehler eingeschlichen: Auf Seite 1, Zeile 3 von unten muss es N statt M heissen. Die Dateien unten sind bereits korrigiert.

15.1.99: Auf den Linux-Rechnern am CIP-Pool ist das Tableauverfahren 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.

Vorsicht: Der unless-Operator hat in ptl eine andere ("reflexive") Semantik als in der Vorlesung: Statt "<" wird dort in der Semantikdefinition immer "<=" verwendet.

14.12.98: Die Definition der beiden temporalen Strukturen in Aufgabe 17 enthielt leider einen Fehler: es muss "m+1" statt "m" heissen. Die Dateien unten sind bereits korrigiert.

Inhalt

Die temporale Logik ist eine Erweiterung der klassischen mathematischen Logik, bei der Aussagen zu verschiedenen Zeitpunkten verschiedene Wahrheitswerte haben können. Die Vorlesung gibt eine ausführliche Einführungen in Theorie und Anwendungen dieser Logik bis hin zu neueren Entwicklungen. Einige Stichworte:

Lineare und verzweigte temporale Logik, TLA
Transitionssysteme und temporale Theorien
Spezifikation und Verifikation paralleler Programme mit temporaler Logik
Model checking

Die Vorlesung ist für das Hauptstudium ausgelegt. Grundkenntnisse in Mathematischer Logik sind hilfreich.

Personen

Die Vorlesung wird im Wintersemester 1998/99 von Prof. Dr. Fred Kröger gehalten. Die Übungen werden von Dr. Stephan Merz betreut.

Termine

Montag      11-13 Uhr    Vorlesung   Raum  037, Oettingenstr.67  BEGINN 2.11.
Donnerstag  12-14 Uhr    Vorlesung   Raum   23, Oettingenstr.67
Freitag     13-15 Uhr    Übung       Raum  131, Oettingenstr.67  BEGINN 13.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
M. Abadi, S. Merz: On TLA as a Logic. In: M. Broy (Hrsg.): Deductive Program Design. Springer-Verlag, 1996
S. Merz: A User's Guide to TLA. Sommerschule Modélisation et vérification des processus parallèles, Nantes 1998.

Übungsbetrieb

Die Übungsblätter werden in der Vorlesung am Donnerstag verteilt. Die Aufgaben werden am Freitag 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 Freitag, den 13.11.1998 statt.

Klausur und Schein

Voraussetzung zum Erwerb des Übungsscheins sind 50% der mit Punkten versehenen Hausaufgaben sowie das Bestehen der Klausur. Näheres zu Termin und Ort der Klausur wird zu gegebener Zeit bekanntgegeben.

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.)

Bei Fragen und Vorschlägen bitte email an Stephan Merz.

Lehrstuhl

Institut

Universität

Stephan Merz (12.10.98)