Technische Universität Ilmenau

Verifikation - Modultafeln der TU Ilmenau

Die Modultafeln sind ein Informationsangebot zu unseren Studiengängen. Rechtlich verbindliche Angaben zum Verlauf des Studiums entnehmen Sie bitte dem jeweiligen Studienplan (Anlage zur Studienordnung). Bitte beachten Sie diesen rechtlichen Hinweis. Angaben zum Raum und Zeitpunkt der einzelnen Lehrveranstaltungen entnehmen Sie bitte dem aktuellen Vorlesungsverzeichnis.

Fachinformationen zu Verifikation im Studiengang Bachelor Informatik 2013
Fachnummer101182
Prüfungsnummer2200470
FakultätFakultät für Informatik und Automatisierung
Fachgebietsnummer 2241 (Automaten und Logik)
Fachverantwortliche(r)Prof. Dr. Dietrich Kuske
TurnusSommersemester
SpracheDeutsch
Leistungspunkte5
Präsenzstudium (h)34
Selbststudium (h)116
VerpflichtungWahlpflicht
Abschlussmündliche Prüfungsleistung, 20 Minuten
Details zum Abschluss
max. Teilnehmerzahl
Vorkenntnisse

endliche Automaten (vgl. z. B. Automaten, Sprachen und Komplexität), Aussagen- und Prädikatenlogik (vgl. z. B. Logik und Logikprogrammierung)

Lernergebnisse

Die Studenten kennen die Verfahren des Model Checkings mittels temporaler Logiken LTL, CTL und CTL*. Sie kennen die Beschränkungen dieser Logiken bzgl. Ausdrucksstärke und Resourcenverbrauch der Entscheidungsverfahren. Sie können ähnliche temporale Logiken bzgl. dieser Kriterien bewerten.

Inhalt

LTL, CTL und CTL* für endliche Kripkestrukturen, OBDDs, LTL für Kellersysteme

Medienformen

Tafel

Literatur

Clark, Grumberg, Peled: Model Checking, MIT Press 2000.

 

Gabbay, Hodkinson, Reynolds: Temporal Logic, Ox. Univ. Press 1994.

 

Emerson: Temporal und Modal Logic. In: J. van Leeuwen (Ed.): Handbook of Theoretical Computer Science, Chapter 16, Amsterdam 1990.

Lehrevaluation

Pflichtevaluation:

 

Freiwillige Evaluation:

WS 2016/17 (Übung)

Informationen und Handreichungen zur Pflege von Modul- und Fachbeschreibungen durch den Modul- oder Fachverantwortlichen finden Sie auf den Infoseiten zum Modulkatalog.