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

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