MSO queries on tree decomposable structures are computable with linear delay

Abstract

LiNEAR-DELAYlin is the class of enumeration problems computable in two steps: The first step is a precomputation in linear time in the size of the input and the second step computes successively all the solutions with a delay between two consecutive solutions y1 and y2 that is linear in |y2|. We prove that evaluating a fixed monadic second order (MSO) query φ(X̄) (i.e. computing all the tuples that satisfy the MSO formula) in a binary tree is a LlNEAR-DELAYlin problem. More precisely, we show that given a binary tree T and a tree automaton F representing an MSO query φ(X̄), we can evaluate F on T with a preprocessing in time and space complexity O(|Γ|3|T|) and an enumeration phase with a delay O(|S|) and space O(max\S\) where |S| is the size of the next solution and max|S| is the size of the largest solution. We introduce a new kind of algorithm with nice complexity properties for some algebraic operations on enumeration problems. In addition, we extend the precomputation (with the same complexity) such that the ith (with respect to a certain order) solution S is produced directly in time O(|S| log(|T|)). Finally, we generalize these results to bounded treewidth structures. © Springer-Verlag Berlin Heidelberg 2006.