:: What is EACSL
:: CSL Conferences
:: Ackermann Award
:: Alonzo Church Award
:: CSL Bibliography
Ackermann Award 2005: Mikolaj Bojanczyk
CitationMikolaj Bojanczyk receives the 2005 Ackermann Award of the European Association of Computer Science Logic (EACSL) for his thesis
Decidable Properties of Tree Languages
Background of the thesisThe automata theoretic and logical study of tree properties has two branches, depending on whether one considers finite or infinite trees. Despite their common origin in the analysis of monadic second-order logic (MSO) over trees in the fundamental papers by Doner, Thatcher/Wright, Rabin, and others, the two research directions have developed in different ways and with different domains of application.
A motivating challenge for the the first part of Bojancyk's thesis is to find an analogue of Schutzenberger's Theorem for trees. More generally, the goal is to decide whether a given regular tree language belongs to some fixed definability class of trees. This is a very ambitious goal. Indeed, while this kind of definability problems are well-understood for words, and despite the fact that the theory of tree languages and tree automata is a bustling field, with close ties to verification and model checking, the question of deciding, or even characterising first-order definability of tree languages has not seen any progress for many years -- not for lack of interest, but because previous efforts by doctoral students and experienced researchers alike in the 1990s had been inconclusive. A possible explanation for this is that in the case of words, these questions are tackled through an algebraic approach. In the case of trees, the algebraic approach is much more difficult and much less developed.
The motivating challenges for the second part of Bojancyk's thesis are extensions of Rabin's Theorem on the decidability of the monadic theory of the infinite binary tree and their applications to program logics and games.
Bojanczyk's thesisThe thesis Decidable Properties of Tree Languages by M. Bojanczyk represents an important advance in the classification theory of regular sets of finite trees, and secondly it introduces an intriguing extension of MSO-logic over infinite trees with interesting applications in programming logics.
The first part deepens our understanding of various logics over finite trees, in particular first-order logic (including the partial tree ordering < in the signature) and chain logic (where second-order variables only range over sets that are linearly ordered by <). Other systems are temporal logics like CTL* or fragments thereof. After about twenty years of little progress, the results of the thesis provide an important step forward in the aim of fixing syntactic invariants that allow to decide for a given MSO-property whether it is expressible in such a fragment. Bojanczyk develops a new machinery to study these questions:
These concepts and results are beautiful and represent real innovations. The results are then applied to characterize effectively the tree languages definable by three different fragments of CTL*, in which the temporal operators are restricted to EX, EF, respectively the use of both (but excluding the until" construct). The given characterizations are very attractive for the effective criteria they provide, and they are technical master-pieces for the corresponding completeness proofs.
The second part of the thesis addresses the search for proper extensions of Rabin's Theorem that the monadic theory of the infinite binary tree (S2S) is decidable. There are two approaches: to change the model (e.g., by considering certain infinite graphs instead of the binary tree), or to modify the means of quantification. The thesis follows the second path, rather neglected up to now in the literature.
Mikolaj Bojanczyk introduces an interesting new quantifier B which allows to sharpen the existence of finite sets by the requirement that their size has to be bounded. Two decidability results on the satisfiability question are shown: first for the closure of MSO-logic by B, the existential quantifier plus the connectives "or", "and", secondly for the MSO-formulas preceded by the dual U-quantifier. The proof offers the interesting idea of "quasi-regular" tree languages which are shown to be the appropriate basis for B-quantification. The central contribution of the chapter is the set-up of a subtle balance between expressiveness and decidability. This is very convincingly documented in three different applications: the finite satisfiability problem for the two-way mu-calculus, the bounded tree-width problem for graphs defined inside the full binary tree, and solving pushdown games with stack unboundedness conditions.
The thesis is written in a very concise and fresh style and conveys a spirit of original thought and intuitive clarity.
Biographic SketchMikolaj Bojanczyk was born on 8th June, 1977. He studied computer science in Warsaw where he graduated in 2000 with a M.Sc. thesis on two-way alternating automata. For this thesis he obtained the second prize in a national competition of the Polish Informatics Society for best M.Sc. awards in Computer Science. Between 200 and 2004 he was a Phd student, also at Warsaw, under the supervision of Igor Walukiewicz. He is currently a post-doc researcher at University Paris 7.
His brilliant dissertation is not the only point of excellence in Bojanczyk's work. His results on tree-walking automata, jointly with Colcombet and completely independent of the dissertation, solved a long-standing open problem and got a best paper award at ICALP 2004.