Lics

IEEE Symposium on Logic in Computer Science

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

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}
 }