학술논문
Higher-order recursion schemes and collapsible pushdown automata: logical properties.
Document Type
Journal
Author
Broadbent, Christopher H. (4-OX-DCS) AMS Author Profile; Carayol, Arnaud (F-UGE-LIG) AMS Author Profile; Ong, C.-H. Luke (4-OX-DCS) AMS Author Profile; Serre, Olivier (F-UPARIS-IRI) AMS Author Profile
Source
Subject
03 Mathematical logic and foundations -- 03B General logic
03B70Logic in computer science
68Computer science -- 68Q Theory of computing
68Q42Grammars and rewriting systems
68Q45Formal languages and automata
03B70
68
68Q42
68Q45
Language
English
Abstract
Summary: ``This article studies the logical properties of a very general class of infinite ranked trees, namely, those generated by higher-order recursion schemes. We consider, for both monadic second-order logic and modal $\mu$-calculus, three main problems: model-checking, logical reflection (a.k.a. global model-checking, that asks for a finite description of the set of elements for which a formula holds), and selection (that asks, if exists, for some finite description of a set of elements for which an MSO formula with a second-order free variable holds). For each of these problems, we provide an effective solution. This is obtained, thanks to a known connection between higher-order recursion schemes and collapsible pushdown automata and on previous work regarding parity games played on transition graphs of collapsible pushdown automata.''