Verification - Interaktive Studienpläne der TU Ilmenau
Die Interaktiven Studienpläne sind ein Informationsangebot zu den Studiengängen der TU Ilmenau.
Die rechtsverbindlichen Studienpläne entnehmen Sie bitte den jeweiligen Studien- und Prüfungsordnungen (Anlage Studienplan).
Alle Angaben zu geplanten Lehrveranstaltungen finden Sie im elektronischen Vorlesungsverzeichnis.
Bitte beachten Sie, dass auf dieser Seite keine Aktualisierungen mehr vorgenommen werden. Alle Module und Studienpläne ab der PO-Version 2021 (Bachelor- und Master-Studiengänge) sind ab sofort im Campus-Portal erreichbar.
| Modulinformationen zu Verification im Studiengang Master Ingenieurinformatik 2021 | |
|---|---|
| Modulnummer | 200048 |
| Prüfungsnummer | 2200693 |
| Fakultät | Fakultät für Informatik und Automatisierung |
| Fachgebietsnummer | 2241 (Automaten und Logik) |
| Modulverantwortliche(r) | Prof. Dr. Dietrich Kuske |
| Turnus | Wintersemester |
| Sprache | Englisch |
| Leistungspunkte | 5 |
| Präsenzstudium (h) | 34 |
| Selbststudium (h) | 116 |
| Verpflichtung | Wahlmodul |
| Abschluss | mündliche Prüfungsleistung, 20 Minuten |
| Details zum Abschluss | |
| Link zum Moodle-Kurs | https://moodle.tu-ilmenau.de/course/view.php?id=3563 |
| Lehrende | Prof. Kuske |
| Anmeldemodalitäten für alternative PL oder SL | |
| max. Teilnehmerzahl | |
| Vorkenntnisse | endliche Automaten: NFAs, DFAs, Konstruktionen hierzu (vgl. z. B. Modul "Automaten und Formale Sprachen") _________________________________________ finite automata (NFAs, DFAs), pushdown automata, related constructions (cf. e.g. module "automata and formal languages") |
| Lernergebnisse und erworbene Kompetenzen | The students know the system model of a finite Kripke structure, a pushdown system, a (lossy) channel systen and a well-structures transition system. They know the basic verification problems reachability, recurrent reachability and the model checking problem for termporal logics. They are familiar with the algorithmic possibilities and limitations in handling these problems as well as with the expressive power of temporal logics. They can evaluate temporal logics wrt. these criteria and adapt the methods to similar system models.
The students can clearly formulate critical questions regarding the topics covered, regarding problems wrt. understanding the material and regarding the solutions of exercise questions. They can clearly advance their view in discussion with both, other students and teaching staff. |
| Inhalt | reachability, recurrent reachability, model checking temporal logics finite Kripke structures, (lossy) channel systems, well-structured transition systems |
| Medienformen und technische Anforderungen bei Lehr- und Abschlussleistungen in elektronischer Form | board, exercise sheets |
| 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 | |