Verification - Interactive curriculae of TU Ilmenau
The interactive curriculae provide information on the degree programmes offered by the TU Ilmenau.
Please refer to the respective study and examination rules and regulations for the legally binding curricula (Annex Curriculum).
You can find all details on planned lectures and classes in the course catalogue.
Please note that this page is no longer updated. All modules and study plans from PO version 2021 onwards (Bachelor and Master study programs) are now available on the Campus Portal.
| module properties Verification in degree program Master Informatik 2021 | |
|---|---|
| module number | 200048 |
| examination number | 2200693 |
| department | Department of Computer Science and Automation |
| ID of group | 2241 (Automata and Logics) |
| module leader | Prof. Dr. Dietrich Kuske |
| term | winter term only |
| language | Englisch |
| credit points | 5 |
| on-campus program (h) | 34 |
| self-study (h) | 116 |
| obligation | elective module |
| exam | oral examination performance, 20 minutes |
| details of the certificate | |
| link to Moodle course | https://moodle.tu-ilmenau.de/course/view.php?id=3563 |
| teacher | Prof. Kuske |
| signup details for alternative examinations | |
| maximum number of participants | |
| previous knowledge and experience | 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") |
| learning outcome | 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. |
| content | reachability, recurrent reachability, model checking temporal logics finite Kripke structures, (lossy) channel systems, well-structured transition systems |
| media of instruction and technical requirements for education and examination in case of online participation | board, exercise sheets |
| literature / references | 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 |
| evaluation of teaching | |