|
| This Article | ||
| ||
| Share | ||
| Bibliographic References | ||
| Add to: | ||
| | ||
| Search | ||
| ||
| ASCII Text | x | ||
| C.-H. L. Ong, "On Model-Checking Trees Generated by Higher-Order Recursion Schemes," Logic in Computer Science, Symposium on, pp. 81-90, 21st Annual IEEE Symposium on Logic in Computer Science (LICS'06), 2006. | |||
| BibTex | x | ||
| @article{ 10.1109/LICS.2006.38, author = {C.-H. L. Ong}, title = {On Model-Checking Trees Generated by Higher-Order Recursion Schemes}, journal ={Logic in Computer Science, Symposium on}, volume = {0}, year = {2006}, issn = {1043-6871}, pages = {81-90}, doi = {http://doi.ieeecomputersociety.org/10.1109/LICS.2006.38}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, } | |||
| RefWorks Procite/RefMan/Endnote | x | ||
| TY - CONF JO - Logic in Computer Science, Symposium on TI - On Model-Checking Trees Generated by Higher-Order Recursion Schemes SN - 1043-6871 SP81 EP90 A1 - C.-H. L. Ong, PY - 2006 KW - null VL - 0 JA - Logic in Computer Science, Symposium on ER - | |||
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.
