On Model-Checking Trees Generated by Higher-Order Recursion Schemes

We prove that the modal mu-calculus model-checking problem for (ranked and ordered) node-labelled trees that are generated by order-n recursion schemes (whether safe or not, and whether homogeneously typed or not) is nEXPTIME complete, for every n ≥ 0. It follows that the monadic second-order theories of these trees are decidable. There are three major ingredients. The first is a certain transference principle from the tree generated by the scheme – the value tree – to an auxiliary computation tree, which is itself a tree generated by a related order-0 recursion scheme (equivalently, a regular tree). Using innocent game semantics in the sense of Hyland and Ong, we establish a strong correspondence between paths in the value tree and traversals in the computation tree. This allows us to prove that a given alternating parity tree automaton (APT) has an (accepting) run-tree over the value tree iff it has an (accepting) traversal-tree over the computation tree. The second ingredien...

• Type: Conference
• Year: 2006
• Where: LICS
• Authors: C.-H. Luke Ong
• Keywords: Computation Tree, Computer Science, LICS 2006, Recursion Scheme, Value Tree