POPL 2025 (series) / VMCAI 2025 (series) / 26th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2025) /
Space-Efficient Model-Checking of Higher-Order Recursion Schemes
Model checking trees generated by order-k Higher-Order Recursion Schemes (HORS) against Alternating Parity Tree-Automata (APT) is known to be a k-EXPTIME-complete problem (Ong’06). We exhibit a natural fragment of HORS, called tail-recursive HORS, and a restricted APT model, called bounded-alternation APT,such that the problem of model checking trees generated by order-k tail-recursive HORS against bounded-alternation APT is k-1-EXPSPACE-complete. The upper bound is achieved by converting the problem into an alternating reachability game, the lower one via a reduction from a tiling problem.
Mon 20 JanDisplayed time zone: Mountain Time (US & Canada) change
Mon 20 Jan
Displayed time zone: Mountain Time (US & Canada) change
14:00 - 15:30 | |||
14:00 30mTalk | Space-Efficient Model-Checking of Higher-Order Recursion Schemes VMCAI 2025 Florian Bruse University of Kassel | ||
14:30 30mTalk | Parameterized Verification of Systems with Precise (0,1)-Counter Abstraction VMCAI 2025 Paul Eichler CISPA - Helmholtz Center for Information Security, Swen Jacobs CISPA, Chana Weil-Kennedy IMDEA Software Institute | ||
15:00 30mTalk | Property-agnostic base case extension for scalable verification of distributed systems VMCAI 2025 |