Abstract
We show a new simple algorithm that solves the modelchecking problem for recursion schemes: check whether the tree generated by a given higherorder 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 n1, 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 nEXPTIME, 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 modelchecking problem.
Our transformation is a generalization of a previous transformation of the author (2020), working for reachability automata in place of parity automata. The stepbystep approach can be opposed to previous algorithms solving the considered problem "in one step", being compulsorily more complicated.
BibTeX  Entry
@InProceedings{parys:LIPIcs.ICALP.2021.140,
author = {Parys, Pawe{\l}},
title = {{HigherOrder Model Checking Step by Step}},
booktitle = {48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)},
pages = {140:1140:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959771955},
ISSN = {18688969},
year = {2021},
volume = {198},
editor = {Bansal, Nikhil and Merelli, Emanuela and Worrell, James},
publisher = {Schloss Dagstuhl  LeibnizZentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2021/14209},
URN = {urn:nbn:de:0030drops142098},
doi = {10.4230/LIPIcs.ICALP.2021.140},
annote = {Keywords: Higherorder recursion schemes, Parity automata, Modelchecking, Transformation, Order reduction}
}
Keywords: 

Higherorder recursion schemes, Parity automata, Modelchecking, Transformation, Order reduction 
Collection: 

48th International Colloquium on Automata, Languages, and Programming (ICALP 2021) 
Issue Date: 

2021 
Date of publication: 

02.07.2021 