|
Published Articles >> Table of Contents >> Abstract
21st Annual IEEE Symposium on Logic in Computer Science (LICS'06)
pp. 81-90
On Model-Checking Trees Generated by Higher-Order Recursion Schemes
C.-H. L. Ong, Oxford University, UK
Full Article Text:

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/LICS.2006.38
Send link to a friend
| 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.
|
Additional Information
|
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
|
|