Institut für Informatik	WS 2006/2007
LMU München	Prof. Dr. F. Kröger
	M. Hammer

Temporale Logik und Zustandssysteme

Klausurergebnisse

Geordnet nach den letzten beiden Ziffern der Matrikelnummer:

Matrikelnr	Punkte	Note
...09	17	3.7
...18	10	5.0
...49	6	5.0
...50	17	3.7
...75	27	2.0
...79	28	1.7
...81	18	3.3
...88	17	3.7
...95	20	3.0

Eine Klausureinsicht ist am 21.2.2007 um 14:00Uhr im Raum E0.9 möglich. Bei dieser Gelegenheit können auch die Scheine abgeholt werden. Später können die Scheine bei Prof. Kröger in der regulären Sprechstunde abgeholt werden.

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.

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)

Materialien

Kurzskriptum zur Vorlesung: Komplettes Skriptum
Übungsblätter: Blatt 1 - Lösungsvorschlag; Blatt 2 - Lösungsvorschlag; Blatt 3 - Lösungsvorschlag; Blatt 4 - Lösungsvorschlag; Blatt 5 - Lösungsvorschlag; Blatt 6 - Lösungsvorschlag; Blatt 7 - Lösungsvorschlag; Blatt 8 - Lösungsvorschlag; Blatt 9 - Lösungsvorschlag; Blatt 10 - Lösungsvorschlag; Blatt 11 - Lösungsvorschlag; Blatt 12 - Lösungsvorschlag; Blatt 13 - Lösungsvorschlag
Klausur: Angabe - Lösungsvorschlag

Termine

Vorlesung: 4-stündig; Mo 12-14 Uhr, Ort: Oettingenstr. 67, Raum 1.35; Di 12-14 Uhr, Ort: Oettingenstr. 67, Raum 1.35; Beginn: 1. Woche (16.10.2006)
Übung: 2-stündig; Mi 12-14 Uhr, Ort: Oettingenstr. 67, Raum 1.35; Beginn: 2. Woche (25.10.2006)
Klausur: 2-stündig, Open Book; 7.2.2007; 12-14 Uhr, Ort: Oettingenstr. 67, Raum 1.35

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 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.

Die Bearbeitung der Hausaufgaben kann in Gruppen bis zu drei Personen vorgenommen werden.

Moritz Hammer (07.08.2006)

Last modified: Thu Feb 15 17:53:00 CET 2007