Enumeration of Monadic Second-Order Queries on Trees

摘要

We consider the enumeration problem of Monadic Second-Order (MSO) queries with first-order free variables over trees. In Bagan [2006] it was shown that this problem is in CONSTANT-DELAY_lin. An enumeration problem belongs to CONSTANT-DELAY_lin if for an input structure of size n it can be solved by: -an O(n) precomputation phase building an index structure, -followed by a phase enumerating the answers with no repetition and a constant delay between two consecutive outputs. In this article we give a different proof of this result based on the deterministic factorization forest decomposition theorem of Colcombet [2007].