Columbia University
IN THE CITY OF NEW YORK COMPUTER SCIENCE
Mihalis Yannakakis (212) 939-7145 mihalis@cs.columbia.edu
February 10, 2013
Prof. Jan Kratochvil
Faculty of Informatics
Masaryk University
Office for Research and Development
Botanická 68a
60200 Brno
Czech Republic
Dear Professor Kratochvil,
This is an evaluation of the Habilitation thesis of Tomas Brazdil, entitled "How to Efficiently Play with Infinitely Many States". In brief, my assessment is that this is an excellent habilitation thesis on important problems of current interest.
The thesis investigates classes of stochastic games with two players and an infinite number of states, which are induced by given finite descriptions. The thesis studies several such types of games. One line of work concerns stochastic PDA (pushdown automata) games. For the general class of PDA games, basic problems (e.g. termination) are undecidable, so the thesis studies two important subclasses: games where the PDA has only one state, termed stochastic BPA games, and games where there is only one symbol in the stack alphabet (i.e. the stack is a counter), termed stochastic one-counter games. The thesis addresses basic termination and reachability problems for these games, and presents complexity and algorithmic results.
The thesis next investigates (nonstochastic) games with multiple counters, termed eVASS and a subclass called VASS, which are in a sense a game-theoretic extension of vector addition systems. It also studies a subclass, called consumption games, which model the consumption and replenishment of resources. The thesis presents results concerning the decidability and complexity
er Science Building   Mail Code 0401   1214 Amsterdam Avenue   New York, NY 10027   212-939-7000   Fax 212-666-0140
of basic questions regarding safety objectives where the goal is to avoid the reduction of the counter values to 0.
Finally the thesis studies systems with stochastically generated tasks. Two such models are studied. One concerns the offline or online scheduling of a stochastically generated task system with the objectives of minimizing the expected completion time or space. The second one is a controlled branching queuing network model, with the objective of ensuring the stability of the network.
The thesis constitutes a significant advance in our understanding of infinite-state games and in the development of methods for their analysis. The models are interesting, several of them were introduced by Dr. Brazdil and his coauthors, they extend other well-studied models, and they are certainly worthy of investigation.
The work is of very high quality, and is characterized by technical depth and rigor. The results have been presented in a series of papers (9 papers are included in the collection) that appeared in prestigious, highly selective conferences such as the ACM-SIAM Symposium on Discrete Algorithms (SODA), the International Symposium on Automata, Languages and Programming (ICALP), the Symposium on Theoretical Aspects of Computer Science (STACS), the International Conference on Computer-Aided Verification (CAV), and the International Conference on Concurrency Theory (CONCUR).
The thesis is organized very well. The definitions and results are presented in a clear, systematic way with pointers to the relevant literature. The second part of the thesis includes the underlying papers with the detailed proofs.
In summary, this is an excellent Habilitation thesis. I recommend its acceptance. There is no doubt that it meets and exceeds the requirements for a habilitation thesis in the field of Informatics.
Mihalis Yannakakis
Percy K. and Vida L. W. Hudson Professor of Computer Science
Computer Science Building   Mail Code 0401   1214 Amsterdam Avenue   New York, NY 10027   212-939-7000   Fax 212-666-0140
Sincerely,