Higher-order recursion schemes are systems of rewrite rules on typed non-terminal symbols, which can be used to define infinite trees. The Global Modal Mu-Calculus Model Checking Problem takes as input such a recursion scheme together with a modal μ-calculus sentence and asks for a finite representation of the set of nodes in the tree generated by the scheme at which the sentence holds. Using a method that appeals to game semantics, we show that for an order-n recursion scheme, one can effectively construct a non-deterministic order-n collapsible pushdown automaton representing this set. The level of the automaton is strict in the sense that in general no non-deterministic order-(n∈-∈1) automaton could do likewise (assuming the requisite hierarchy theorem). The question of determinisation is left open. As a corollary we can also construct an order-n collapsible pushdown automaton representing the constructible winning region of an order-n collapsible pushdown parity game. © 2009 Springer Berlin Heidelberg.
CITATION STYLE
Broadbent, C., & Ong, L. (2009). On global model checking trees generated by higher-order recursion schemes. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5504 LNCS, pp. 107–121). https://doi.org/10.1007/978-3-642-00596-1_9
Mendeley helps you to discover research relevant for your work.