Rewriting Higher-Order Stack Trees

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 satisfaction of any formula written in monadic second order logic (respectively first order logic with reachability predicates) can be decided on such a graph. We unify both models by introducing the notion of stack trees, whose nodes are labelled by higher-order stacks, and define the corresponding class of higher-order closed tree rewriting systems. These graphs retain the decidability properties of ground tree rewriting graphs while generalising the pushdown hierarchy of graphs.

Authors

• Vincent Penelle

Keywords

No keywords are indexed for this paper.