Jakob Piribauer
jakob.piribauer[at]tu-dresden.de
back to main
Teaching Summer 2024, University of Leipzig
Formal verification aims to provide guarantees that a (software or hardware) system behaves as intended. To this end, algorithms are developed that automatically check whether the system satisfies certain formal specifications.
The behavior of complex systems is often non-deterministic and probabilistic. Non-determinism arises , e.g., due to the interaction with an unknown environment or due to concurrency. Probabilism, on the other hand, can be caused, for instance, by randomization explicitly used in algorithm or when probabilities of component failures are known or can be estimated.
This course covers model-checking techniques for the quantitative analysis of models of such systems. The formal models used are Markov chains (purely probabilistic) and Markov decision processes (probabilistic and non-deterministic. The course covers:
- Basics of Markov chains and Markov decision processes
- Computation of reachability probabilities, steady-state probabilities, expected rewards
- Probabilistic computation tree logic (PCTL) and model-checking algorithms
- Insights into ongoing research in the field
Literature
Several of the topics covered in the course can be found in Chapter 10 of
"Principles of model checking", Christel Baier and Joost-Pieter Katoen; MIT press, 2008.
Prerequisites
Knowledge of basic probability theory as well as general mathematical skills are presumed.
Knowledge of formal verification and model checking in the non-probabilistic setting is advantageous, but not necessary.
Place and time
Lecture: Tuesday, 11:15 - 12:45, Hörsaal 19 (Hörsaalgebäude, Augustusplatz)
Exercise class: Tuesday, 15:15 - 16:45 (A-Woche), SG 3-11 (Seminargebäude, Augustusplatz)
Modalities are expressions that quantify the truth of a statement, e.g., 'possibly' and 'necessarily'. Modal logics are simple, yet expressive, formalisms that incorporate such modalities. The incorporated modalities offer a wide variety of possible readings such as temporal readings ('at some point in the future ...'), epistemic readings ('the agent knows that ...'), or readings talking about the dynamics of programs ('there is an execution of program P after which ...'). Therefore, modal logics are useful in various application domains and play an important role in computer science, philosophy, mathematics, and linguistics among others.
This course provides an introduction to the main concepts of modal logic with a focus on its role in computer science. It covers:
- syntax and semantics of modal logics,
- Kripke structures and Kripke frames,
- bisimulations and invariance results,
- frame definability,
- soundness and completeness results,
- complexity and decidability results,
- propositional dynamic logic.
Literature
The course follows the book
"Modal logic (Fourth printing with corrections)", Patrick Blackburn, Maarten de Rijke, Yde Venema; Cambridge University Press, 2010.
Prerequisites
For the course, basic knowledge on first-order logic and complexity theory as well as elementary mathematical knowledge and skills are presumed.
Place and time
Lecture: Thursday, 11:15 - 12:45, Hörsaal 19 (Hörsaalgebäude, Augustusplatz)
Exercise Class: Tuesday, 15:15 - 16:45 (B-Woche), SG 3-11 (Seminargebäude, Augustusplatz)
Game theory is a discipline playing an important role in mathematics, economics, and computer science. This seminar covers a selection of topics of game theory in computer science. These topics will span from theoretical concepts important in game theory to algorithmic solutions to different kinds of (abstract) games.
Literature
"Algorithmic Game Theory", Noam Nisan, Tim Roughgarden, Eva Tardos, Vijay V. Vazirani; Cambridge University Press, 2007.
"Multiagent systems: Algorithmic, game-theoretic, and logical foundations", Yoav Shoham and Kevin Leyton-Brown; Cambridge University Press, 2008.
"Games on Graphs", Nathanaël Fijalkow; available online: https://arxiv.org/abs/2305.10546, 2023.
Time
The seminar will take place on July 16 and 17, 2024. An initial meeting will take place on April 18, 2024, at 14:50. Details have been sent to the participants.