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


Katedra informačních technologií
prof. RNDr. Antonín Kučera, Ph.D.
Tel.: +420-549 49 4374
Email: tony(atsign)fi(dot)muni(dot)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)