Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

On Higher-Order Reachability Games vs May Reachability

Kazuyuki Asada, Hiroyuki Katsura, Naoki Kobayashi

TL;DR

It is shown that reachability games for order-n programs can be reduced to may-reachability for order-(n+1) programs, and vice versa, and formalize the reductions by using higher-order fixpoint logic and prove their correctness.

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.

On Higher-Order Reachability Games vs May Reachability

TL;DR

It is shown that reachability games for order-n programs can be reduced to may-reachability for order-(n+1) programs, and vice versa, and formalize the reductions by using higher-order fixpoint logic and prove their correctness.

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.
Paper Structure (18 sections, 16 theorems, 62 equations, 3 figures, 1 table)

This paper contains 18 sections, 16 theorems, 62 equations, 3 figures, 1 table.

Table of Contents

  1. Introduction
  2. $\mu$HFL(Z) and Reachability Problems
  3. Syntax
  4. Semantics of $\mu$HFL(Z) Formulas
  5. Relationship with Reachability Problems
  6. Main Theorem
  7. From Order-$n$ Reachability Games to Order-($n+1$) May-Reachability
  8. From Order-($n+1$) May-Reachability to Order-$n$ Reachability Games
  9. Intuitions for the Order-1 Case
  10. Translation for the General Case
  11. Correctness
  12. Reduction to the Recursion-free Case
  13. Reduction Relation with Explicit Substitution
  14. Correctness in the Recursion-free Case
  15. Applications
  16. ...and 3 more sections

Key Result

Theorem 2.3

For any closed simply-typed term $M$ of type $\mathtt{unit}$ and order $k$, $M^\dagger$ is a closed $\mu$HFL(Z) formula of type $\star$ and order $k$. The player $\mathtt{P}$ wins the reachability game for $M$, if and only if, $\mathop{[\![}M^\dagger\mathop{]\!]}=\top$.

Figures (3)

  • Figure 1: Simple Type System for $\mu$HFL(Z)
  • Figure 2: Simple Type System for the Language.
  • Figure 3: Translation from order-($n+1$) disjunctive $\mu$HFL(Z) to order-$n$$\mu$HFL(Z).

Theorems & Definitions (22)

  • Example 2.2
  • Theorem 2.3: DBLP:conf/pepm/WatanabeTO019
  • Example 2.4
  • Theorem 2.5
  • Example 3.1
  • Theorem 3.2
  • Lemma 3.3
  • Corollary 3.4
  • Lemma 3.5
  • Lemma 3.6
  • ...and 12 more