## Paper: On model-checking trees generated by higher-order recursion schemes (at LICS 2006)

**C.-H. Luke Ong**

### Abstract

We prove that the modal mu-calculus model-checking problem for (ranked and ordered) node-labelled trees that are generated by order- recursion schemes (whether safe or not, and whether homogeneously typed or not) is - EXPTIME complete, for every n \geqslant 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 ingredient is the simulation of an (accepting) traversal-tree by a certain set of annotated paths over the computation tree; we introduce traversal-simulating APT as a recognising device for the latter. Finally, for the complexity result, we prove that traversal-simulating APT enjoy a succinctness property: for deciding acceptance, it is enough to consider run-trees that have a reduced branching factor. The desired bound is then obtained by analysing the complexity of solving an associated (finite) acceptance parity game.

### BibTeX

@InProceedings{Ong-Onmodelcheckingtree, author = {C.-H. Luke Ong}, title = {On model-checking trees generated by higher-order recursion schemes}, booktitle = {Proceedings of the Twenty-First Annual IEEE Symposium on Logic in Computer Science (LICS 2006)}, year = {2006}, month = {August}, pages = {81--90}, location = {Seattle, Washington, USA}, publisher = {IEEE Computer Society Press} }