Rewriting Higher-Order Stack Trees

TL;DR

This paper introduces stack trees, unifying higher-order pushdown systems and ground tree rewriting systems, and demonstrates that their generated graphs preserve decidability properties, extending the pushdown hierarchy.

Contribution

The paper defines stack trees and higher-order ground tree rewriting systems, generalizing existing models while maintaining key decidability features.

Findings

Graphs generated by these systems are decidable for monadic second order logic.

The model generalizes the pushdown hierarchy of graphs.

Decidability properties are preserved in the new framework.

Abstract

Higher-order pushdown systems and ground tree rewriting systems can be seen as extensions of suffix word rewriting systems. Both classes generate infinite graphs with interesting logical properties. Indeed, the model-checking problem for monadic second order logic (respectively first order logic with a reachability predicate) is decidable on such graphs. We unify both models by introducing the notion of stack trees, trees whose nodes are labelled by higher-order stacks, and define the corresponding class of higher-order ground tree rewriting systems. We show that these graphs retain the decidability properties of ground tree rewriting graphs while generalising the pushdown hierarchy of graphs.