NDLI: On Model-Checking Trees Generated by Higher-Order Recursion Schemes

Content Provider	IEEE Xplore Digital Library
Author	Ong, C.-H.L.
Copyright Year	2006
Description	Author affiliation: Comput. Lab., Oxford Univ. (Ong, C.-H.L.)
Abstract	We prove that the modal mu-calculus model-checking problem for (ranked and ordered) node-labelled trees that are generated by order-n recursion schemes (whether safe or not, and whether homogeneously typed or not) is n-EXPTIME complete, for every nges0. 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
Sponsorship	IEEE Comput. Soc. Tech. Committ. on Mathematical Found. of Comput
Starting Page	81
Ending Page	90
File Size	360567
Page Count	10
File Format	PDF
ISBN	0769526314
ISSN	10436871
DOI	10.1109/LICS.2006.38
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2006-08-12
Publisher Place	USA
Access Restriction	Subscribed
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	Tree graphs Automata Logic Safety Laboratories Computational modeling Embedded computing Algorithm design and analysis Computer science Game theory
Content Type	Text
Resource Type	Article
Subject	Mathematics Software

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Collapsible Pushdown Automata and Recursion Schemes

Winning Regions of Higher-Order Pushdown Games

A Type System Equivalent to the Modal Mu-Calculus Model Checking of Higher-Order Recursion Schemes

On model-checking trees generated by higher-order recursion schemes.

On global model checking trees generated by higher-order recursion schemes (2009).

On model-checking trees generated by higher-order recursion schemes

On model-checking trees generated by higher-order recursion schemes (2006)

Higher-Order Model Checking: From Theory to Practice

Model Checking and Functional Program Transformations

On Model-Checking Trees Generated by Higher-Order Recursion Schemes

Similar Documents

Collapsible Pushdown Automata and Recursion Schemes

Winning Regions of Higher-Order Pushdown Games

A Type System Equivalent to the Modal Mu-Calculus Model Checking of Higher-Order Recursion Schemes

On model-checking trees generated by higher-order recursion schemes.

On global model checking trees generated by higher-order recursion schemes (2009).

On model-checking trees generated by higher-order recursion schemes

On model-checking trees generated by higher-order recursion schemes (2006)

Higher-Order Model Checking: From Theory to Practice

Model Checking and Functional Program Transformations

On Model-Checking Trees Generated by Higher-Order Recursion Schemes