MSO queries on tree decomposable structures are computable with linear delay. (English) Zbl 1225.68268
Ésik, Zoltán (ed.), Computer science logic. 20th international workshop, CSL 2006, 15th annual conference of the EACSL, Szeged, Hungary, September 25–29, 2006. Proceedings. Berlin: Springer (ISBN 978-3-540-45458-8/pbk). Lecture Notes in Computer Science 4207, 167-181 (2006).
Summary: Linear-Delay\(_{\text{lin}}\) 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 \(y_{1}\) and \(y_{2}\) that is linear in \(|y_{2}|\). We prove that evaluating a fixed monadic second-order (MSO) query \(\varphi(\bar{X})\) (i.e., computing all the tuples that satisfy the MSO formula) in a binary tree is a Linear-Delay\(_{\text{lin}}\) problem. More precisely, we show that given a binary tree \(T\) and a tree automaton \(\Gamma \) representing an MSO query \(\varphi(\bar{X})\), we can evaluate \(\Gamma \) on \(T\) with a preprocessing in time and space complexity \(O(|\Gamma |^{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 \(i^{\text{th}}\) (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.
For the entire collection see [Zbl 1130.68007].
For the entire collection see [Zbl 1130.68007].
MSC:
68W05 | Nonnumerical algorithms |
03D05 | Automata and formal grammars in connection with logical questions |
68Q25 | Analysis of algorithms and problem complexity |
68R05 | Combinatorics in computer science |