Modulcode:	infAutLog-01a
Englische Bezeichnung:	Automata and Logics
Modulverantwortliche(r):	Prof. Dr. Thomas Wilke
Turnus:	unregelmäßig (SS23 SS24)
Präsenzzeiten:	4V 2Ü
ECTS:	8
Workload:	60 Std. Vorlesung, 30 Std. Präsenzübung, 150 Std. Selbststudium
Dauer:	ein Semester
Modulkategorien:	MSc-Inf-Theo (MSc Inf (21)) MSc-Inf-WP (MSc Inf (21)) 2F-MEd-Inf-WP (MEd-Hdl Inf (21)) 2F-MA-Inf-WP (2F-MA Inf (21))
Lehrsprache:	Englisch
Voraussetzungen:	infBL-01a infAAK-01a

Kurzfassung:

This course covers advanced topics in automata theory and logic in computer science.

Lernziele:

The topics listed below are inspired by practical questions in computer science. As they aim at establishing (in a formal sense) the correct functioning of software and hardware, a formal framework with an accopanying theory is required.

Students

• explain the ideas and the exact formal frameworks -- theories -- of the various approaches and the reasoning behind them and
• adapt the theories to new situations and extend them to cover new situations.

Lehrinhalte:

• context-free and deterministic context-free languages [1]
• linear-time temporal logic, automata on infinite words, and model checking [2]
• model checking probabilistic systems [2]
• complexity of solving word equations [3, 4]
• completeness of a natural proof system [5, 6]
• decidability of Presburger arithmetic [7]
• relative completeness of Hoare logic [8]
• SAT solver, SMT solver, and program verification [9]

Weitere Voraussetzungen:

Prüfungsleistung:

Depending on the number of students:

• portfolio (in combination with a short presentation as a prerequisite)
• oral exam (with a preceding working phase)
• written exam.

Lehr- und Lernmethoden:

• lecture: presentations by lecturer and discussions/work in small groups
• classroom exercise: discussion of solutions of/approaches to home problems

Verwendbarkeit:

Only one of the following modules can be credited to the same degree programme: infFLog-01a: Fortgeschrittene Logik in der Informatik, infLICS2-01a: Logic in Computer Science - Advanced oder infAutLog-01a: Automata and Logics.

Literatur:

[1] I. Chiswell. 2009. A course in formal languages, automata and groups. Springer, London.

[2] Chr. Beier, J.-P. Katoen. 2008. Principles of Model Checking. MIT Press, Cambridge, MA.

[3] M. Lothaire et al. 2002. Algebraic Combinatorics on Words. Encyclopedia of Mathematics and its Applications. Cambridge University Press, Cambridge, UK.

[4] A. Jez. 2017. Word Equations in Nondeterministic Linear Space. In 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017), July 10-14, 2017, Warsaw, Poland. LIPIcs, Vol. 80. Schloss Dagstuhl - Leibniz-Zentrum für Informatik.

[5] M. Huth, M. Ryan. 2012. Logic in Computer Science. Cambridge University Press, Cambridge.

[6] H.-D. Ebbinghaus, J. Flum, W. Thomas. 2021. Mathematical Logic, 3rd Ed. Springer, New York.

[7] C. Haase. 2018. A survival guide to Presburger arithmetic. ACM SIGLOG News 5, 3, 67-82.

[8] M. Gordon. 2016. Background reading on Hoare Logic, lecture notes, 2016.

[9] L. De Moura, N. Bjørner. 2011. Satisfiability modulo theories: introduction and applications. Communications of the ACM 54, 9, 69-77.

Verweise:

Kommentar:

Shared course: Dirk Nowotka and Thomas Wilke.

Alternative prerequisite: Inf-TGI and Inf-LogInf.