Space-Efficient Model-Checking of Higher-Order Recursion Schemes

Explore a research presentation on space-efficient model-checking techniques for higher-order recursion schemes delivered at VMCAI 2025. In this 31-minute video, Florian Bruse from the University of Kassel introduces a natural fragment called tail-recursive HORS and a restricted Alternating Parity Tree-Automata model with bounded alternation. Learn how model checking trees generated by order-k tail-recursive HORS against bounded-alternation APT achieves k-1-EXPSPACE-completeness, improving upon the known k-EXPTIME-complete complexity of the general problem established by Ong in 2006. The presentation demonstrates both upper bounds through conversion to alternating reachability games and lower bounds via reduction from tiling problems. This technical talk was presented at the VMCAI conference in January 2025 and sponsored by ACM SIGPLAN.