Papers

23. Effective characterizations of tree logics (tutorial at PODS 2008) (Corrections)
A survey. Known results of the form: a regular tree language can be defined in logic A if and only if the tree automton satisfies property B.

22. Piecewise testable tree languages (LICS 2008),
joint work with Luc Segoufin and Howard Straubing
A tree version of the Simon theorem on piecewise testable word languages. The word theorem says that a word language has a J-trivial syntactic monoid if and only if it is a finite boolean combination of languages "words with w as a (possibly not connected) subword". In the tree version, the algebraic property is not J-triviality, but a more restrictive condition.

21. Tree-walking automata (tutorial at LATA 2008)
A survey of tree-walking automata. The main focus is on how the expressive power is changed by adding features such as pebbles or nondeterminism.

20. XPath evaluation in linear time (PODS 2008),
joint work with Paweł Parys
An algorithm that finds the set of nodes in a document that satisfy a given XPath query. The algorithm is designed for a rich fragment of XPath, which talks about attribute values. The algorithm runs in time linear in the size of the tree, and not in quadratic time, as previous approaches. This comes at a cost, though: the constant in the linear time is exponential in the size of the query.

19. The common fragment of ACTL and LTL (FoSSaCS 2008)
A sort of paradox. The language "all paths belong to (ab)*a(ab)*c^\omega" can be defined in CTL, but necessarily using existential modalities. In particular, ACTL (the fragment of CTL witout existential modalities) does not capture the intersection of LTL and CTL. The paper also includes a decidable characterization of languages of infinite words that can be defined by a formula of \Sigma_2.

18. Forest algebra (Automata and Logic: History and Perspectives. Collected papers for Wolfgang Thomas' 60th birthday),
joint work with Igor Walukiewicz
This paper introduces a new model for regular languages of unranked trees. The model is meant to be for trees that which semigroups are for words.

17. Forest expressions (CSL 2007)
This paper introduces a model of regular expression for unranked trees. The main focus is on connections with logic: the expressions correspond to chain logic, the star-free expressions correspond to first-order logic, and finally, a concatenation hierarchy is shown to correspond to the quantifier alternation hierarchy.

16. Shuffle expressions and words with nested data (MFCS 2007),
joint work with Henrik Bjoerklund
We introduce a plethora of models, which are connected to words with several data values. Possibly the nicest result is an emptiness procedure for a formalism that can define, among other things, the set of words a^{n1}#...#a^{nk}b^{m1}#...#b^{mk}, where k>0 and n1,...,nk is a permutation of m1,...mk.

15. A new algorithm for testing if a regular language is locally threshold testable (IPL)
The paper gives an alternative algorithm for deciding if a regular language is locally threshold testable. The idea is not to use algebra, but Parikh images.

14. Reachability in Unions of Commutative Rewriting Systems is Decidable
joint work with Piotr Hoffman (STACS 2007)
We take two commutative rewriting systems (systems where there is a rule ab->ba for every two letters a,b; essentially multiset rewriting), and add their rules together. The result may no longer be commutative, but we show that reachability is still decidable.

13. Two-way unary temporal logic over trees (LICS 2007)
The logic considered has two modalities: "exists a descendant with \phi" and "exists an ancestor with \phi". I show that the following problem is decidable: decide if a given regular tree language can be defined in two-way unary temporal logic. This is part of a larger program, whose goal is to understand the expressive power of tree logics, preferrably in terms of decision procedures.

12. Bounded depth data trees
joint work with Henrik Bjoerklund (ICALP 2007)
As in paper [11], we consider data trees. We show that if a bound is fixed on the depth of trees, then problems that could not be solved in [11] can be shown decidable. The main tool is priority multicounter automata of K. Reinhardt, these are an extended form of Petri nets.

11. Two-variable logic on data trees and applications to XML reasoning,
joint work with Claire David, Anca Muscholl, Thomas Schwentick and Luc Segoufin (PODS 2006)
We consider data trees: these are finite trees, with labels, and data values. The latter are modelled as an equivalence relation on tree nodes. We show that a two-variable logic has decidable satisfiability over such models; this result is then applied to some XML tasks. "Best paper" at PODS 2006.

10. Two-variable logic on words with data,
joint work with Claire David, Anca Muscholl, Thomas Schwentick and Luc Segoufin (LICS 2006)
We consider data words: these are like the data trees above, only they are words. We give a decidable (w.r.t. emptiness) two-variable logic. Differences with respect to [11]: a) the logic is stronger, by allowing order and successor, instead of just successor; b) we develop a reasonable automaton model; c) we do infinite words, as well.

9. Bounds in omega-regularity,
joint work Thomas Colcombet (LICS 2006)
A continuation of [5]. We consider an extension of monadic second-order logic over infinite words. The extension comes from adding a "bounding quantifier", and can express properties such as: whenever P occurs, then Q occurs with bounded delay. We develop an automaton model, as well as regular expressions, that capture some, but not all, properties expressible in the logic. There is a very complicated complementation argument in the paper.

8. Expressive power of pebble automata,
joint work with Mathias Samuelides, Thomas Schwentick and Luc Segoufin (ICALP 2006)
We show some upper bounds on the expressive power of pebble automata (tree-walking automata that can mark tree nodes with pebbles). The main result is that pebble automata cannot recognize all regular tree languages.

7. TWA do not recognize all regular languages,
joint work with Thomas Colcombet (SIAM Journal of Computing)
Tree-walking automata are a sequential (non-branching model) for recognizing tree languages. The automata can be compiled into branching automata, but the converse fails, as this paper shows. This is the journal version of a STOC 2005 paper.

6. TWA cannot be determinized,
joint work with Thomas Colcombet (TCS)
(journal version of ICALP 2004 paper) We give a language that can be recognized by a nonterministic TWA, but not a deterministic one. The conference version was "Best paper" at ICALP 2004.

5. A bounding quantifier (CSL 2004)
This paper introduces the bounding quantifier later studied in [9]. Satisfiability is shown decidable for a fragment (much smaller than that in [9]). However, the models are infinite trees, and not infinite words.

4. Characterizing EF and EX Tree Logics,
joint work with Igor Walukiewicz (TCS)
(journal version of CONCUR 2004 paper) These are results similar to [13]. We consider two modalities: "exists a descendant with \phi", and "exists a successor with \phi", and three logics, depending on which of the two modalities are used. We give a decidable characterization for each of the three logics. The proofs are obfuscated, since binary trees are used. A cleaner proof for unranked trees is in [18].

3. 1-bounded TWA cannot be determinized (FSTTCS 2003)
A partial result, made obsolete by [6].

2. Two-way alternating automata and finite models (ICALP 2002)
We consider the modal mu-calculus, with forward and backward modalities. This calculus no longer has the finite model property, and I show that it is EXPTIME-complete to decide if a given formula has a finite model.

1. The finite model problem for alternating two-way automata (TCS 298:3)
(journal version of FOSSACS 2001 paper) A partial result, made obsolete by [2]. Here I considered a fragment of the calculus that corresponds to the Buchi condition, and not full parity, as in [2].

Decidable properties of tree languages (under Igor Walukiewicz)
The thesis corresponds to papers [2], [4] and [5], with some further observations on first-order and chain logic on finite trees.