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

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. Key words...

• Type: Conference
• Year: 2009
• Where: FOSSACS
• Authors: Christopher Broadbent, C.-H. Luke Ong
• Keywords: Applied Computing, Collapsible Pushdown Automaton, FOSSACS 2009, Order-n Collapsible Pushdown, Recursion Scheme