Universität München
Institut für Informatik
Lehr- und Forschungseinheit für Programmierung und Softwaretechnik
`www.pst.informatik.uni-muenchen.de/Lehre/SS01/tl/`

Temporale Logik und Zustandssysteme (PG)

Aktuelles

Am Donnerstag, 26.07.2001, findet noch eine Vorlesung statt. Dabei wird zunächst das Thema CTL-Modelchecking abgeschlossen, danach gibt es einen Ausblick auf das Modelchecking-Praktikum und mögliche Themen für Fortgeschrittenenpraktika und Diplomarbeiten.

Klausurergebnisse

( Angabenblatt / Lösungsvorschlag)

Matrikelnummer	Note
090574304370	1,0
071076301074	1,3
050674301789	n.best.
200574304971	3,7
200575304127	3,7
021237301894	4,0
051175304140	n.best.
250377403598	n.best.
131275304380	2,0

Inhalt

Zustandsübergangssysteme bilden einen sehr allgemeinen Sammelbegriff für alle Arten von Systemen, die ablaufen können, wobei ein Ablauf eine Folge von Zuständen ist. Beispiele (aus der Informatik) sind Programme bzw. allgemeinere Software-Systeme, Schaltkreise, Datenübertragungsprotokolle, Automaten, Petri-Netze usw.

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. Praktische Relevanz hat die temporale Logik im Zusammenhang mit model checking erfahren, einer Sammlung von automatischen Analysetechniken für Hard- und Softwaresysteme.

Die Vorlesung gibt eine ausführliche Einführung in verschiedene Varianten dieser Logik (lineare und verzweigte Temporallogik) und entwickelt systematisch ihre Anwendungsmöglichkeiten im Bereich der Spezifikation und Verifikation (einschließlich model checking) von Systemen.

Personen

Die Vorlesung und die Übungen werden im Sommersemester 2001 von Dr. Stephan Merz gehalten.

Termine

Montag      12:15-13:45 Uhr    Vorlesung   Raum  E45,  Theresienstr. 39
Montag      14:15-15:45 Uhr    Übung       Raum  E45,  Theresienstr. 39
Donnerstag   9:15-10:45 Uhr    Vorlesung   Raum  E46,  Theresienstr. 39

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.

Ferner wird während der Vorlesung ausführliches Begleitmaterial ausgegeben.

23.04.01	Begleitblatt 1
03.05.01	Begleitblatt 2
10.05.01	Begleitblatt 3
10.05.01	Begleitblatt 4
07.06.01	Begleitblatt 5
11.06.01	Begleitblatt 6
18.06.01	Begleitblatt 7
21.06.01	Begleitblatt 8
25.06.01	Begleitblatt 9
28.06.01	Begleitblatt 10
02.07.01	Begleitblatt 11
09.07.01	Begleitblatt 12
16.07.01	Begleitblatt 13
16.07.01	Begleitblatt 14
19.07.01	Begleitblatt 15

Übungsbetrieb, Klausur und Schein

Die Klausur fand am Montag, 23.07.01, um 12:15 im Raum E45 in der Theresienstr. 39 statt. Hier sind das Angabenblatt und der Lösungsvorschlag.

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

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