Higher-Order Model Checking Step by Step

I will show a new simple algorithm that solves the model-checking problem for recursion schemes: check whether the tree generated by a given higher-order recursion scheme is accepted by a given alternating parity automaton. Recursion scheme is a formalism to represent/generate an infinite tree, extending regular trees and context-free trees. A recursion scheme is defined similarly to a context-free grammar, but nonterminals can take arguments, which can be used on the right side of rules (and the arguments can again take further arguments). Recursion schemes are equivalent to simply-typed lambda-calculus with recursion, and to collapsible pushdown automata (an extension of pushdown automata). The model-checking problem is known to be decidable, and more precisely n-EXPTIME-complete for schemes of order n; moreover, it is in FPT when arity of nonterminals and the size of the automaton are parameters. I will present a new algorithm achieving the same complexity bounds, but being simpler from previous algorithms. The algorithm amounts to a transformation from a recursion scheme of order n to an (exponentially larger) recursion scheme of order n-1, where the answer to the model-checking question remains unchanged. The talk is based on a my paper "Higher-Order Model Checking Step by Step" published on ICALP 2021.