loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
21st Annual IEEE Symposium on Logic in Computer Science (LICS'06)
On Model-Checking Trees Generated by Higher-Order Recursion Schemes
Seattle, Washington
August 12-August 15
ISBN: 0-7695-2631-4
C.-H. L. Ong, Oxford University, UK
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.

Citation:
C.-H. L. Ong, "On Model-Checking Trees Generated by Higher-Order Recursion Schemes," lics, pp.81-90, 21st Annual IEEE Symposium on Logic in Computer Science (LICS'06), 2006
Usage of this product signifies your acceptance of the Terms of Use.