Temporale Logik und Zustandssysteme
Aktuell
Scheine können bei Dirk Pattinson, Zi. E 0.9 abgeholt
werden, jedoch nicht
- zwischen 25.3. und 29.3.,
- zwischen 5.4. und 9.4.,
- zwischen 19.4. und 23.4.
Die Ergebnisse der Klausur vom
10.2. 2004 liegen vor.
Termine
- Vorlesung:
-
Dienstags, 12-14 Uhr, Raum 1.31, Oettingenstraße 67
Donnerstags, 12-14 Uhr, Raum 17, Oettingenstraße 67,
Beginn 12:00
- Übung:
- Montags, 12-14 Uhr, Raum 0.13, Oettingenstraße 67
(Beginn 27.10.2003)
- Kurztests:
- Montag, 15.12.2003, 18-19 Uhr, Raum 1.35, Oettingenstraße 67
- Montag, 26.1.2004, 18-19 Uhr, Raum 1.35, Oettingenstraße 67
- Klausur:
- Dienstag, 10.2.2004, 18-20 Uhr, Raum E 52, Theresienstraße 39
Materialien
Folien zur Vorlesung
Kalenderwoche 43: Teil 1 [.pdf],
Teil 2 [.pdf].
Kalenderwoche 44: [.pdf].
Kalenderwoche 45: Teil 1 [.pdf],
Teil 2 [.pdf].
Kalenderwoche 46: [.pdf].
Kalenderwoche 47: Teil 1 [.pdf],
Teil 2 [.pdf].
Kalenderwoche 48: [.pdf].
Kalenderwoche 49: Teil 1 [.pdf],
Teil 2 [.pdf].
Kalenderwoche 50: Teil 1 [.pdf],
Teil 2 [.pdf].
Kalenderwoche 51: [.pdf].
Kalenderwoche 01, 2004: [.pdf].
Kalenderwoche 02, 2004: Teil 1 [.pdf],
Teil 2 [.pdf].
Kalenderwoche 03, 2004: [.pdf].
Kalenderwoche 04, 2004: [.pdf].
Kalenderwoche 05, 2004: [.pdf].
Kalenderwoche 06, 2004: [.pdf].
Kalenderwoche 07, 2004: [.pdf].
Übunsgblätter, Lösungsvorschläge
Blatt 1 [.pdf],
Lösungsvorschlag [.pdf].
Blatt 2 [.pdf],
Lösungsvorschlag [.pdf].
Blatt 3 [.pdf],
Lösungsvorschlag [.pdf].
Blatt 4 [.pdf],
Lösungsvorschlag [.pdf].
Blatt 5 [.pdf],
Lösungsvorschlag [.pdf].
Blatt 6 [.pdf],
Lösungsvorschlag [.pdf].
Blatt 7 [.pdf],
Lösungsvorschlag [.pdf].
Blatt 8 [.pdf],
Lösungsvorschlag [.pdf].
Blatt 9 [.pdf],
Lösungsvorschlag [.pdf].
Blatt 10 [.pdf],
Lösungsvorschlag [.pdf].
Blatt 11 [.pdf],
Lösungsvorschlag [.pdf].
Blatt 12 [.pdf],
Lösungsvorschlag [.pdf].
Blatt 13 [.pdf],
Lösungsvorschlag [.pdf].
Kurztests, Lösungsvorschläge
Kurztest 1 (Gruppe A [.pdf],
Gruppe B [.pdf]),
Lösungsvorschlag [.pdf].
Kurztest 2 (Gruppe A [.pdf],
Gruppe B [.pdf]),
Lösungsvorschlag [.pdf].
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
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.
Scheinerwerb
Übungsscheine können durch die erfolgreiche Teilnahme
einer Klausur am Semesterende erworben werden.
Die Voraussetzung für die Teilnahme an der Klausur ohne
Maluspunkte ist das Erreichen von 50 % der Punkte in zwei
Kurztests Mitte Dezember und Ende Januar. Beide Kurztests werden
gleich gewichtet; es wird der das Mittel der in beiden Klausuren
erreichten Punktzahl gewertet.
Teilnehmer, die nicht 50 % der Punkte in den Kurztests
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
Kurztests fehlt, muss ein Prozentpunkt mehr in der Klausur erreicht
werden, um sie zu bestehen.
Beispiel:
- Ohne Malus:In den Kurztests wurden mindestsns 50% der
Punkte erreicht. Dann ist die Klausur bestanden, wenn mindestens 50 % der
Klausurpunkte erreicht werden.
- Mit Malus: In den Kurztests wurde (beispielsweise) nur
43 % der Gesamtpunktzahl erreicht. Dann ist die Klausur bestanden,
wenn mindestens 57 = 50 + (50 - 43) % der Klausurpunkte erreicht
werden.
Ergebnisse
Dirk Pattinson
(Wednesday, 24-Mar-2004 17:10:54 CET).