Stochastic processes and games
The aim of formal analysis of real-world systems is to reveal their key features. For example, a system for air traffic management should be safe, efficient and cheap. All these features can be algorithmically analyzed once we create a formal model of the system in a suitable mathematical formalism. Each system has its own specific properties that affect the choice of the formalism. Many systems exhibit a special form of unpredictability, called quantified uncertainty: sometimes the next state of the system is not determined but we may estimate the probability of moving to particular states. A trivial example is a simple coin tossing: we cannot say which side will be face-up but we know that the probability of "head" is 1/2 (we ignore the possibility that the coin lands on its edge).
Systems exhibiting the quantified uncertainty are modeled using stochastic processes. Among the most useful models are various kinds of Markov chains with discrete as well as continuous time evolution. Markov chains are often applied in various contexts. For example, they can be used to model users of an Internet browser (such model forms the basis of Google PageRank), credibility of clients of financial institutions, biological processes, etc. They allow analysis of many properties from the probability of incorrect behavior of a system to computation of system average load.
Many real-world systems need to be controlled in some way or another. Such systems are often found in industry. An important task is to design a controller which would control the system in the best way. Controlled systems that exhibit a quantified uncertainty can be modeled using so called decision processes and stochastic games. Formal analysis of a decision process or a game results in a strategy which achieves optimal results. For example such a strategy minimizes the probability of collision of two aircraft and/or minimizes the cost of the air traffic management system.
The main research topics
- Recursive stochastic processes
We study probabilistic extensions of pushdown automata, machines with counters, parallel processes, etc. Our goal is to investigate fundamental properties of such systems, for example the probability and the mean time of reaching a given set of states. General results obtained for such processes can be applied in other areas, e.g. in queueing theory, planning, analysis of randomized algorithms and data structures, etc.
- Multiplayer games on transition systems
We concentrate on a special type of turn-based games in which every player has its own goal, not necessarily conflicting with goals of other players (such a goal can be e.g. maximization of the probability of reaching a given set of states). We study basic properties of such games e.g. existence of equilibria, complexity of computing optimal strategies, etc.
- Stochastic real-time systems
Here we mostly concentrate on the so called generalized semi-Markov processes (that are equivalent to stochastic Petri nets). We study effects of imposing time constraints upon such systems. We usually express these constraints using timed automata and develop algorithms for their verification.
- Specification formalisms for stochastic processes
We are investigate fundamental properties of formalisms that are suitable for specification of desired behavior of stochastic processes. We mostly concentrate on various temporal logics (e.g. PCTL) and formalism based on automata theory (e.g. timed automata as a specification language for continuous time processes). Our goal is to design suitable formalisms for specification of important properties as well as algorithmic verification of such properties.
Information for students
Stochastic processes and games constitute a modern and very attractive field of research, which can be successfully done even by undergraduate students (some of our doctoral students published their first papers during their master's studies). The research is relatively demanding and suitable mainly for "mathematically oriented" students. More information can be obtained from any member of our team.
Our team
The head of the team:
Antonín Kučera
Employees:
Tomáš Brázdil,
Vojtěch Řehák
PhD students:
Jan Krčál,
Jan Křetínský,
Petr Novotný,
Ivana Hutařová Vařeková
Former PhD students:
Václav Brožek,
Vojtěch Forejt,
Contact
Tel.: +420-549 49 4374
Email: tonyfimunicz
http://www.fi.muni.cz/usr/kucera/
http://iti.fi.muni.cz/
Awards received by members of our team
The following awards have been received by members of our team:- 2010 Vojtěch Forejt
- Newton International Fellowship, British Academy of Sciences, Royal Society
- 2009 Václav Brožek
- Newton International Fellowship, British Academy of Sciences, Royal Society
- 2009 Jan Křetínský
- Rector's award for the best master's students of MU
- 2008 Tomáš Brázdil
- Beth dissertation award
- 2008 Vojtěch Forejt
- Rector's award for the best PhD students of MU
- 2007 Tomáš Brázdil
- Humboldt fellowship
- 2007 Tomáš Brázdil
- Rector's award for the best PhD students of MU
- 2007 Václav Brožek
- Rector's award for the best master's students of MU
- 2007 Vojtěch Forejt
- 2. place in the competition SVOČ (theoretical computer science)
- 2007 Václav Brožek
- 2. place in the competition SVOČ (theoretical computer science)
- 2003 Tomáš Brázdil
- 1. place in the competition SVOČ (theoretical computer science)