-
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
Module INF-56-52-M-6
Advanced Automata Theory (M, 8.0 LP)
Module Identification
Module Number | Module Name | CP (Effort) |
---|---|---|
INF-56-52-M-6 | Advanced Automata Theory | 8.0 CP (240 h) |
Basedata
CP, Effort | 8.0 CP = 240 h |
---|---|
Position of the semester | 1 Sem. in SuSe |
Level | [6] Master (General) |
Language | [EN] English |
Module Manager | |
Lecturers | |
Area of study | [INF-ALG] Algorithmics and Deduction |
Reference course of study | [INF-88.79-SG] M.Sc. Computer Science |
Livecycle-State | [NORM] Active |
Courses
Type/SWS | Course Number | Title | Choice in Module-Part | Presence-Time / Self-Study | SL | SL is required for exa. | PL | CP | Sem. | |
---|---|---|---|---|---|---|---|---|---|---|
4V+2U | INF-56-52-K-6 | Advanced Automata Theory
| P | 84 h | 156 h |
U-Schein
| ja | PL1 | 8.0 | SuSe |
- About [INF-56-52-K-6]: Title: "Advanced Automata Theory"; Presence-Time: 84 h; Self-Study: 156 h
- About [INF-56-52-K-6]: The study achievement [U-Schein] proof of successful participation in the exercise classes (ungraded) must be obtained. It is a prerequisite for the examination for PL1.
Examination achievement PL1
- Form of examination: written exam (Klausur) (60-180 Min.)
- Examination Frequency: Examination only within the course
- Examination number: 65652 ("Advanced Automata Theory")
Evaluation of grades
The grade of the module examination is also the module grade.
Contents
Competencies / intended learning achievements
Upon successful completion of the module, students will be able to
- model reactive systems with automata,
- specify the correctness with logical formulas,
- derive verification algorithms,
- transfer the procedures to similar system models.
Literature
Will be announced during the lecture.
Requirements for attendance (informal)
None
Requirements for attendance (formal)
None
References to Module / Module Number [INF-56-52-M-6]
Course of Study | Section | Choice/Obligation |
---|---|---|
[INF-88.79-SG] M.Sc. Computer Science | Computer Science Theory | [WP] Compulsory Elective |
[INF-88.79-SG] M.Sc. Computer Science | Formal Fundamentals | [WP] Compulsory Elective |
[INF-88.79-SG] M.Sc. Computer Science | Specialization 1 | [WP] Compulsory Elective |
[MAT-88.105-SG] M.Sc. Mathematics | Subsidiary Topic (Minor) | [WP] Compulsory Elective |