Module Handbook

  • Dynamischer Default-Fachbereich geändert auf INF

Course INF-56-52-K-6

Advanced Automata Theory (4V+2U, 8.0 LP)

Course Type

SWS Type Course Form CP (Effort) Presence-Time / Self-Study
- K Lecture with exercise classes (V/U) 8.0 CP 156 h
4 V Lecture 56 h
2 U Exercise class (in small groups) 28 h
(4V+2U) 8.0 CP 84 h 156 h


CP, Effort 8.0 CP = 240 h
Position of the semester 1 Sem. in SuSe
Level [6] Master (General)
Language [EN] English
Area of study [INF-ALG] Algorithmics and Deduction
Livecycle-State [NORM] Active

Possible Study achievement

  • Verification of study performance: proof of successful participation in the exercise classes (ungraded)
  • Details of the examination (type, duration, criteria) will be announced at the beginning of the course.


  • finite-state systems:
    • omega automatons
    • MSO and Büchi theorem
    • LTL and Presburg Arithmetic
  • Recursive programs:
    • pushdown automaton, pre* and post*
    • Bounded Context Switching
    • Tree automatons, Rabin theorem
  • Parameterized systems:
  • Regular Model Checking
  • LTL(MSO)
  • Quotients, abstraction and extrapolation


Will be announced during the lecture.

Requirements for attendance (informal)


Requirements for attendance (formal)


References to Course [INF-56-52-K-6]

Module Name Context
[INF-56-52-M-6] Advanced Automata Theory P: Obligatory 4V+2U, 8.0 LP
Course-Pool Name
[INF-Alg_V-KPOOL-6] Lectures of the teaching area Algorithmics and Deduction