Résumé | 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.
The purpose of this talk is to propose a common extension to both higher-order stack operations and ground tree rewriting. We introduce a model of higher-order ground tree rewriting over trees labelled by higher-order stacks (henceforth called stack trees), which syntactically coincides with ordinary ground tree rewriting at order 1 and with the dynamics of higher-order pushdown automata over unary trees. The rewriting system is obtained through the definition of DAGs of operations.
Our contribution is twofold (apart from the definition of the model):
- define a automaton model over DAGs of operations, and show it is closed under iteration.
- showing that the model checking problem for first-order logic with reachability is decidable for the infinite graphs generated by stack tree rewriting systems. This last proof uses the technique of finite set interpretations presented by Colcombet and Loding. |