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

on YouTube ↗31m

" summary

Shows that checking trees from tail-recursive HORS against bounded-alternation APT drops from k-EXPTIME to (k-1)-EXPSPACE complete. Achieves the upper bound by rewriting schemes into lambda-y form, eliminating argument alternation, and converting the problem into an alternating reachability game; gets rid of automaton alternation via a bounded-component partition. Proves the matching lower bound by a tiling-problem reduction. No implementation or experiments are reported.

AI-written summary · about

" chapters (16)

1. 0:00Higher-order recursion schemes intro
2. 1:05Deriving trees from schemes
3. 2:33Model checking with parity automata
4. 5:00Reducing to parity game
5. 9:07Motivation for space efficiency
6. 11:18Connection to HFL and complexity
7. 12:23Tail recursion examples
8. 14:30Tail recursion in schemes
9. 16:16Alternation in verification game
10. 19:11Defining tail recursion
11. 21:49Eliminating alternation via tail recursion
12. 22:10Bounded alternation in automata
13. 24:20Complexity result and proof
14. 25:24Summary and future work
15. 27:02Q&A on parity colors
16. 28:06Q&A on completeness