The Diagonal Problem for Higher-Order Recursion Schemes is Decidable

TL;DR

This paper proves the decidability of the diagonal problem for higher-order recursion schemes, enabling computation of downward closures and aiding in separability and reachability analyses in complex systems.

Contribution

It establishes the first decidability result for the diagonal problem in higher-order recursion schemes, with implications for automata theory and system verification.

Findings

Decidability of the diagonal problem for higher-order recursion schemes.

Algorithm for computing downward closures of languages recognized by schemes.

Applications to separability problems and reachability analysis.

Abstract

A non-deterministic recursion scheme recognizes a language of finite trees. This very expressive model can simulate, among others, higher-order pushdown automata with collapse. We show decidability of the diagonal problem for schemes. This result has several interesting consequences. In particular, it gives an algorithm that computes the downward closure of languages of words recognized by schemes. In turn, this has immediate application to separability problems and reachability analysis of concurrent systems.