On Higher-Order Reachability Games vs May Reachability
Fuente:
arXiv
Salvato in:
| Autori principali: | , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2022
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866917775010693120 |
|---|---|
| author | Asada, Kazuyuki Katsura, Hiroyuki Kobayashi, Naoki |
| author_facet | Asada, Kazuyuki Katsura, Hiroyuki Kobayashi, Naoki |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2203_08416 |
| institution | arXiv |
| publishDate | 2022 |
| record_format | arxiv |
| spellingShingle | On Higher-Order Reachability Games vs May Reachability Asada, Kazuyuki Katsura, Hiroyuki Kobayashi, Naoki Logic in Computer Science Programming Languages 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. |
| title | On Higher-Order Reachability Games vs May Reachability |
| topic | Logic in Computer Science Programming Languages |
| url | https://arxiv.org/abs/2203.08416 |