Higher-Order Model Checking Step by Step

TL;DR

This paper introduces a step-by-step algorithm for higher-order model checking that reduces the problem to finite parity games, achieving optimal complexity and generalizing previous reachability automata methods.

Contribution

The paper presents a novel step-by-step transformation algorithm for higher-order recursion schemes that simplifies model checking for parity automata, extending prior reachability automata techniques.

Findings

Algorithm transforms recursion schemes of order n to order n-1 preserving acceptance.

Overall complexity is n-EXPTIME, proven to be optimal.

Provides an FPT algorithm under bounded arity and automaton size.

Abstract

We 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. The algorithm amounts to a procedure that transforms a recursion scheme of order $n$ to a recursion scheme of order $n-1$, preserving acceptance, and increasing the size only exponentially. After repeating the procedure $n$ times, we obtain a recursion scheme of order $0$, for which the problem boils down to solving a finite parity game. Since the size grows exponentially at each step, the overall complexity is $n$-EXPTIME, which is known to be optimal. More precisely, the transformation is linear in the size of the recursion scheme, assuming that the arity of employed nonterminals and the size of the automaton are bounded by a constant; this results in an FPT algorithm for the model-checking problem. Our transformation is a generalization of a previous transformation of the author (2020), working for reachability automata in place of parity automata. The step-by-step approach can be opposed to previous algorithms solving the considered problem "in one step", being compulsorily more complicated.