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, 12
00-13
30 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