On Higher-Order Reachability Games vs May Reachability
Logic in Computer Science
2024-09-16 v2 Programming Languages
Abstract
We consider the reachability problem for higher-order functional programs and study the relationship between reachability games (i.e., the reachability problem for programs with angelic and demonic nondeterminism) and may-reachability (i.e., the reachability problem for programs with only angelic nondeterminism). We show that reachability games for order-n programs can be reduced to may-reachability for order-(n+1) programs, and vice versa. We formalize the reductions by using higher-order fixpoint logic and prove their correctness. We also discuss applications of the reductions to higher-order program verification.
Keywords
Cite
@article{arxiv.2203.08416,
title = {On Higher-Order Reachability Games vs May Reachability},
author = {Kazuyuki Asada and Hiroyuki Katsura and Naoki Kobayashi},
journal= {arXiv preprint arXiv:2203.08416},
year = {2024}
}