Annotated Stack Trees

TL;DR

This paper introduces Ground Annotated Stack Tree Rewrite Systems, a model for higher-order program verification that generalizes existing systems and demonstrates that reachability sets are regular and computable within n-EXPTIME.

Contribution

It extends higher-order stack tree models to include fork and join constructs and proves the regularity and complexity bounds of reachability analysis.

Findings

Reachability sets are regular for regular target sets.

Construction complexity is optimal at n-EXPTIME for order-n systems.

Extension to include bounded global communication is possible.

Abstract

Annotated pushdown automata provide an automaton model of higher-order recursion schemes, which may in turn be used to model higher-order programs for the purposes of verification. We study Ground Annotated Stack Tree Rewrite Systems -- a tree rewrite system where each node is labelled by the configuration of an annotated pushdown automaton. This allows the modelling of fork and join constructs in higher-order programs and is a generalisation of higher-order stack trees recently introduced by Penelle. We show that, given a regular set of annotated stack trees, the set of trees that can reach this set is also regular, and constructible in n-EXPTIME for an order-n system, which is optimal. We also show that our construction can be extended to allow a global state through which unrelated nodes of the tree may communicate, provided the number of communications is subject to a fixed bound.