Advanced Search
CS Search Google Search
Subscribers, please login

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

Full Article Text: Download PDF of full textBuy this article

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

Similar Articles

Abstract Contents
Abstract
Citation




Free access to

  • Abstracts
  • Selected PDFs

Electronic subscribers login to:

  • Access HTML/PDFs of full text articles

Subscription information

Get a Web account

Peer Review Notice

Give us Feedback