Rewriting Higher-Order Stack Trees

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. In-deed, the model-checking problem for monadic second order logic (re-spectively 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.
Keywords : stack trees
Document type :
Conference papers
Complete list of metadatas

Cited literature [15 references]  Display  Hide  Download

https://hal-upec-upem.archives-ouvertes.fr/hal-01117753
Contributor : Vincent Penelle <>
Submitted on : Tuesday, September 15, 2015 - 3:39:56 PM
Last modification on : Thursday, July 5, 2018 - 2:45:59 PM
Long-term archiving on : Wednesday, April 26, 2017 - 6:33:19 PM

Files

stack_tree.pdf
Files produced by the author(s)

Identifiers

Citation

Vincent Penelle. Rewriting Higher-Order Stack Trees. CSR 2015, Jul 2015, Listvyanka, Russia. pp.364-397, ⟨10.1007/978-3-319-20297-6_24⟩. ⟨hal-01117753v2⟩

Share

Metrics

Record views

517

Files downloads

158