Universität München
Institut für Informatik
Lehr- und Forschungseinheit für Programmierung und Softwaretechnik
http://www.pst.informatik.uni-muenchen.de/lehre/SS02/tl/

Temporale Logik und Zustandssysteme (PG)

Aktuelles

Klausurergebnisse

Die Scheine können bei Stephan Merz abgeholt werden, bitte kurze email zur Terminvereinbarung.

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. Als spezielle Anwendung wird die Verifikation paralleler Programme behandelt.

Personen

Stephan Merz betreut die Übungen.

Termine

Montag      12:15-13:45 Uhr    Vorlesung   Raum  0.13, Oettingenstr. 67
Dienstag    10:00-11:30 Uhr    Übung       Raum  1.15, Oettingenstr. 67
Donnerstag  11:00-12:30 Uhr    Vorlesung   Raum    15, Oettingenstr. 67

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
• C. Stirling: Modal and temporal properties of processes. New York: Springer-Verlag (Texts in Computer Science), 2001

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

Die in der Vorlesung verteilten Folienkopien sind jetzt auch von hier aus zugänglich.

Kapitel 1-3	Server-Version (PDF)	Lokale Version (ZIP)

Hinweise zur Verwendung der Foliensammlung

Die Folien wurden im PDF-Dokumentformat erstellt und ihre Funktionaliät kann nur im Acrobat Reader voll genutzt werden. Ein Link in das Wörterbuch oder in Übungsaufgaben ist dadurch zu erkennen, daß sich der Mauszeiger in eine Hand mit ausgestrecktem Zeigefinger verwandelt (das ist nur im "Handmodus" möglich; im Zoom- und Textauswahlmodus ist ein Link nicht erkennbar). Es wurden zwei inhaltlich identische Versionen der Folien erstellt: eine lokal herunterladbare, sowie eine vom WWW-Server aufrufbare Version.

Dadurch ergeben sich kleine Unterschiede in der Benutzung:

• Die lokale Version
  Die lokale Version kann als ZIP-Datei heruntergeladen werden, in der sich die Folien, die Übungsblätter und das Wörterbuch befinden (bitte immer darauf achten Dokumente aus derselben Zipdatei zu verwenden, sonst funktionieren Links unter Umständen nicht). Die Dokumente aus der ZIP-Datei müssen im selben Verzeichnis abgelegt werden. Durch Klick auf einen Link wird das entsprechende Übungs- oder Wörterbuchdokument in den Acrobat Reader geladen. Mit Hilfe des Menüpunktes "Document->Go Back" oder dem entsprechenden Knopf in der Menüleiste kann in das Ursprungsdokument zurückgesprungen werden.
• Die Server-Version
  Die Server-Version ist ausschließlich für die Verwendung auf dem WWW-Server gedacht. Die Links der Dokumente der Server-Version verweisen auf die entsprechenden Dokumente auf dem WWW-Server des PST-Lehrstuhls. Leider werden die Sprungziele in den Dokumenten nur erkannt wenn der Acrobat Reader als Plugin im Netscape läuft (andere Browser wurden nicht getestet). Der Weg zurück funktioniert mit dem "Zurück-Knopf" des Browsers; dabei wird leider die ursprüngliche Position im Dokument nicht mehr gefunden.
  Achtung: Die Server-Version versucht bei Benutzung der Links immer das Zieldokument vom WWW-Server des PST-Lehrstuhls zu laden. Dadurch können Online-Gebühren entstehen!

Übungsbetrieb, Klausur und Schein

Zum Selbsttest sind hier das Angabenblatt und der Lösungsvorschlag der Klausur aus dem Jahr 2001 abrufbar.

Die Übungsblätter werden in der Vorlesung am Montag verteilt. Übungsblätter enthalten Präsenzaufgaben und mit (H) gekennzeichnete Hausaufgaben. Die Präsenzaufgaben werden in der Übung am Dienstag besprochen. Die Hausaufgaben sollen in der Übungsstunde der Folgewoche abgegeben werden und werden dann besprochen. Abgegebene Hausaufgaben werden eine Woche später korrigiert zurückgegeben. Hausaufgaben, die mit einer Punktezahl gekennzeichnet sind, sind relevant fuer die Zulassung zur Klausur.

Beginn des Übungsbetriebs am Dienstag, den 23.04.2002.

Die Klausur findet am Donnerstag, 18.07.02, von 10:00-12:00 Uhr im Raum 0.43 (Oettingenstr. 67) statt.

Datum	Übungsblatt	Lösungen Präsenzaufgaben	Lösungen Hausaufgaben
15.04.02	Blatt 1	-	Aufgaben 1-2
22.04.02	Blatt 2	Aufgaben 3-4	Aufgabe 5
29.04.02	Blatt 3	Aufgaben 6-7	Aufgaben 8
06.05.02	Blatt 4	Aufgaben 9-11, Mutex-Protokoll für ptl	Aufgaben 12-13
13.05.02	Blatt 5	Aufgaben 14-15d	Aufgaben 15e-15g
16.05.02	Blatt 6	-	Aufgaben 16-18
27.05.02	Blatt 7	Aufgabe 19	Aufgaben 20-21
03.06.02	Blatt 8	Aufgaben 22-23	Aufgabe 24
10.06.02	Blatt 9	Aufgabe 25	Aufgabe 26
17.06.02	Blatt 10	Aufgabe 27	Aufgabe 28
24.06.02	Blatt 11	Aufgaben 29-30	Aufgabe 31
01.07.02	Blatt 12	Aufgaben 32-34, Spezifikation und Invariantenbeweis für Aufgabe 34 in Isabelle/TLA	Aufgabe 35
08.07.02	Blatt 13	Blatt 13
11.07.02	Blatt 14	Blatt 14