Annex 6: Habilitation thesis reader's report Masaryk University Faculty Field of Habilitation MU Faculty of Informatics Informatics Applicant Affiliation Habilitation Thesis Reader Affiliation RNDr. Tomáš Brázdil, Ph.D. Masaryk University, Faculty of Informatics How To Efficiently Play With Infinitely Many States Professor Peter Bro Miltersen Aarhus University, Denmark Report Text (as large as the reader deems necessary) Set ^c* Reader's questions to answer to defend the habilitation thesis (number of questions is upon reader's consideration) Conclusion Tomáš Brázdil's habilitation thesis of "How To Efficiently Play With Infinitely Many States' does -/$>J^toAmeet the standard requirements for a habilitation thesis in the field of Informatics. In Aarhus on Peter Bro Miltersen (1/ i i______ ..(signature) DEPARTMENT OF COMPUTER SCIENCE FACULTY OF SCIENCE AARHUS UNIVERSITY Assessment of the Habilitation thesis of Tomas Brázdil Department of Computer Science Peter Bro Miltersen Professor Date: 07 February 201 3 Direct Tel.: +45 8942 9333 Fax: +45 8942 5601 E-mail: bromille@cs.au.dk Web: au.dk/en/bromille(5>cs Sender's CVR no.: 31119103 Page 1/2 The habilitation thesis of Tomas Brázdil is entitled "How to efficiently play with infinitely many states". It consists of two parts, a survey of the obtained results of roughly 50 pages, followed by nine published papers. The papers were published between 2006 and 2012 and appeared in computer science conferences and journals of high quality. The work of Tomas Brázdil reported in the habilitation thesis is of a fundamental nature. The present reviewer sees the work as a coherent and substantial contribution to the research program of unifying the theory of discrete stochastic processes, decision processes and two-player zero-sum games with the theory of automata, thereby significantly enriching both of these theories. This research program was initiated in the middle of the last decade and is notably "gaining steam". Tomas Bradzil has been a central figure in the community associated with this research program throughout its existence. The research program is not only fundamental and of great practical importance, but also technically very challenging. The thesis of Tomas Brázdil contains a number of technically very non-trivial and conceptually highly original contributions that makes significant progress towards the coveted "grand unification" of automata theory and the theory of stochastic processes and games. I expect the work reported in the thesis to be thoroughly studied and highly cited in the future, not only in the formal method community, but also in the algorithms community, and the community concerned with discrete stochastic processes and games. The central model of the thesis is the stochastic PDA game, a model general enough to encompass a very wide range of models consid- Department of Computer Tel.: +45 89425600 Science Fax:+45 89425601 Aarhus University E-mail: cs@cs.au.dk Aboqade 34 http://www.cs.au.dk DK-8200 Aarhus N Denmark DEPARTMENT OF COMPUTER SCIENCE FACULTY OF SCIENCE AARHUS UNIVERSITY Page 2/2 ered in the theory of stochastic processes as well as in automata — theory. The most central works of thesis consists of analyzing natu- ral special cases of this model, from a game theoretic as well as form a computational perspective. A particular such case where really impressive progress is made is the case of one-counter stochastic games and one-counter Markov Decision processes, where breakthrough algorithmic results that enable the computation of approximations to the value and of approximately optimal strategies are obtained. These results are very important. It is worth noting that highly esteemed figures in the international research community specializing in algorithmic optimization attempted to obtain similar results and failed. The work of Tomas Brázdil reported in the thesis has deservedly made his name a well-known one in the international community. The habilitation thesis of Tomas Brázdil "How To Efficiently Play With Infinitely Many States" fulfils the standard requirements on a habilitation thesis in Computer Science. Peter Bro Miltersen