Temporale Logik und Zustandssysteme
Aktuelles
Klausur: Donnerstag, 10. Februar 2005, ab 18:00 Uhr s.t. in
Raum 132 in der Theresienstr.
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.
Termine
- Vorlesung:
-
Montag, 12-14 Uhr, Oettingenstr. 67, Raum 1.31,
Donnerstags, 1200-1330 Uhr, Oettingenstr. 67, Raum 1.31
- Übung:
- Freitags, 12-14 Uhr, Oettingenstr. 67, Raum .23
Materialien
Kurzskriptum
Das überarbeitete Kurzskriptum in einer Datei: [.pdf], [.ps]
Übungsblätter, Lösungsvorschläge
- Blatt 1 [.pdf], [.ps]; Lösungsvorschlag [.pdf], [.ps];
- Blatt 2 [.pdf], [.ps]; Lösungsvorschlag [.pdf], [.ps];
- Blatt 3 [.pdf], [.ps]; Lösungsvorschlag [.pdf], [.ps];
- Blatt 4 [.pdf], [.ps]; Lösungsvorschlag [.pdf], [.ps];
- Blatt 5 [.pdf], [.ps]; Lösungsvorschlag [.pdf], [.ps];
- Blatt 6 [.pdf], [.ps]; Lösungsvorschlag [.pdf], [.ps];
- Blatt 7 [.pdf], [.ps]; Lösungsvorschlag [.pdf], [.ps];
- Blatt 8 [.pdf], [.ps]; Lösungsvorschlag [.pdf], [.ps];
- Blatt 9 [.pdf], [.ps];Lösungsvorschlag [.pdf], [.ps];
- Blatt 10 [.pdf], [.ps];Lösungsvorschlag [.pdf], [.ps];
- Blatt 11 [.pdf], [.ps];Lösungsvorschlag [.pdf], [.ps];
- Blatt 12 [.pdf], [.ps];
- Übungsblatt zu Herleitungen [.pdf], [.ps];Lösungsvorschlag [.pdf], [.ps];
Klausuren
- Probeklausur vom 12.1.2005 [.pdf], [.ps];Lösungsvorschlag [.pdf], [.ps];
- Klausur vom 10.2.2005 [.pdf],
[.ps];
Literatur
- 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
- Z. Manna, A. Pnueli: The Temporal Logic of Reactive and
Concurrent Systems. Vol.2: Safety Properties. New York:
Springer-Verlag, 1995
- D. Gabbay, I. Hodkinson, M. Reynolds: Temporal Logic -
Mathematical Foundations and Computational Aspects. Vol. 1.
Oxford: Clarendon Press, 1994
- A. G. Hamilton: Logic for Mathematicians. Cambridge University Press,
1989 (Revised edition)
Scheinerwerb
Übungsscheine können durch die erfolgreiche Teilnahme an
einer Klausur am Semesterende erworben werden.
Die Voraussetzung für die Teilnahme an der Klausur ohne
Maluspunkte ist das Erreichen von 50 % der Punkte aus den
Hausaufgaben.
Teilnehmer, die nicht 50 % der Punkte der Hausaufgabenpunkte erreicht
haben, können trotzdem an der Klausur teilnehmen, ihr
Klausurergebnis wird aber mit Maluspunkten belegt: Für jeden
Prozentpunkt der zum Erreichen der 50 % - Marke in den Hausaufgaben
fehlt, muss ein Prozentpunkt mehr in der Klausur erreicht werden, um
sie zu bestehen.
Klausurergebnis
| Matrikelnummer |
Note |
| 88003721 |
1.7 |
| 57306669 |
5.0 |
| 37904375 |
3.7 |
| 58005607 |
3.3 |
| 127705862 |
2.3 |
| 126605614 |
1.3 |
| 107901010 |
3.3 |
| 117606141 |
3.7 |
| 38203844 |
1.0 |
| 78202588 |
2.0 |
| 87604991 |
3.3 |
Klausureinsicht ist möglich am Dienstag, den 22. Februar 2005
bzw. am Dienstag, den 1. März 2005 jeweils zwischen 14 Uhr und 16
Uhr, im Büro 423 in der Theresienstraße 39, bei
Júlia Zappe. Dort können dann auch die Scheine abgeholt
werden. Später können die Scheine bei Prof. Kröger
abgeholt werden.
Moritz Hammer (17.02.2005)
Last modified: Thu Feb 17 10:55:26 CET 2005