Annex 6: Habilitation thesis reader's report
Masaryk University Faculty
Field of Habilitation
MU Faculty of Informatics Informatics
Applicant Affiliation Habilitation Thesis
RNDr. Tomáš Brázdil, Ph.D.
Masaryk University, Faculty of Informatics
How To Efficiently Play With Infinitely Many States
Reader Affiliation
Professor Igor Walukiewicz LaBRI, France
Report Text (as large as the reader deems necessary)
Reader's questions to answer to defend the habilitation thesis (number of questions is upon reader's consideration)
1.
2.
Conclusion
Tomáš Brazdil's habilitation thesis of "How To Efficiently Play With Infinitely Many States " does —does not meet the standard requirements for a habilitation thesis in the field of Informatics.
In Talence eedex on
LABORATOIRE BORDELAIS DE RECHERCHE EN INFORMATIQUE
Talence, January 31, 2013
Igor Walukiewicz
LABRI, Universite Bordeaux 1 351 cours de la Liberation Universite Bordeaux 1 33405 Talence
Report on the Habilitation Thesis of
Thomas Brazdil
Entitled: How To Efficiently Play With Infinitely Many States
Formal models of systems combining interaction and randomness appear in many contexts. They are important for realistic modeling, and at the same time challenging from theoretical point of view. In the last decade, theoretical computer science community has been intensively working on such models. This habilitation thesis focuses on infinite state models combining interaction and randomness.
The starting point of the thesis is the model of stochastic game: the game aspect models interaction of a system with its environment. The first result, that motivates all further research, is that many good properties of finite stochastic games do not hold anymore in the infinite case: the optimal strategies may not exist, and if they exist they may need to be complicated in a precise technical sense. The thesis is devoted to finding subclasses of games with better properties. The considered games are always finitely presentable since the main challenges concern calculating the value of a game, and finding implementable optimal, or close-to-optimal strategies.
The core of the habilitation thesis considers stochastic games played on graphs of pushdown automata. Positions of such a game are configurations of a pushdown automaton, and moves are given by transitions of the automaton. The simplest winning condition considered is termination: being able to empty the stack. Reachability conditions are a refinement of termination since one also requires to reach a particular state when reaching the empty stack. It is known that in general it
is algorithmically impossible to calculate the value in stochastic pushdown games. The focus of the thesis is on subclasses of such games with better algorithmic properties.
The first subclass of pushdown games are stochastic BPA games where one restricts to automata with one control state. Such a restriction appears in many contexts in the study of pushdown automata. A later chapter of the thesis shows a use of this model for scheduling problems. The author exhibits a striking difference between termination and reachability conditions. While termination conditions are relatively easy to solve, for reachability conditions optimal strategies may not exist and the value cannot be easily expressed by a system of non-linear equations. This negative result is counterbalanced by a series of positive results on qualitative reachability conditions.
One counter stochastic games are another subclass of pushdown games where this time the stack alphabet is required to contain just one letter. So the stack becomes a counter that can be incremented or decremented by a constant. Termination conditions that where quite easy in the BPA case become much more complex to analyze. The author shows that for qualitative objectives one counter games with termination conditions can be solved in nondeterministic polynomial time, and that getting a deterministic algorithm would imply a major conjecture in algorithmic game theory. This is a challenging result proved by a detour through much more complicated winning conditions than termination. For quantitative objectives the author shows that the game values may be irrational, and gives an algorithm for approximating the value of a game.
The second part of the habilitation thesis considers non-stochastic games on extended vector addition systems (eVASS). There are not many classes of infinite state games with reasonable algorithmic properties. Games played on graphs of pushdown automata are one of them. The class proposed here by Thomas Brázdil, is another, and a very different one. The main result of this part is decidability of eVASS games for so-called zero-safety objectives. The other important result of this part concerns the special case where increment transitions are very restricted. It turns out that such games can be solved with relatively efficient algorithms. This, among others, gives new algorithms for energy games modeling a situation when the objective is to maintain a positive level of energy.
The final part of the habilitation thesis concerns scheduling problems of stochastically generated tasks. Such problems have been extensively studied in the literature. The author makes a link between variants of this problem and BPA games. He then explores this link to give a series of results on offline and online scheduling. Finally, an important extension is made to reach controlled branching queueing networks model. The main result is decidability in deterministic polynomial time of the existence of an ergodic scheduler for a given network with a fixed number of queues.
The habilitation thesis consist of a self contained survey of the results accompanied by journal and conference papers on which it is based. The survey is written in an exceptionally clear style. It manages to present the main contributions in a precise way while hiding most of the technicalities from the reader.
As underlined in the overview, this habilitation thesis contains many important results in a very active area of research. The thesis witnesses the coherence of the research, and a clear advance in this difficult subject. In doing this the author shows his command of a remarkably large spectrum of advanced tools. Without doubt Tomas Brazdil is one of the leading researchers in his field. The accompanying publications from prestigious journals and first-rate conferences are an additional witness of the very high quality of the research presented in this habilitation thesis.
Thomas Brazdil's habilitation thesis of "How to Efficiently Play With Infinitely Many States" does meet the standard requirements for a habilitation thesis in the field of Informatics.
Igor Walukiewicz
Directeur de Recherches CNRS
Reader's questions:
1. This question concerns stochastic BPA games from Section 3.1. On page 19 you say that their value for reachability objectives cannot be easily expressed using a system of non-linear equations. Can you explain this point in more detail. Does it imply that it would be very difficult to approximate the value?
2. The question concerns complexity of solving eVASS games as described in Theorem 4.1.3. In the introduction you state that the complexity of solving these games is high. What is know about the lower bound for this problem?