Rewriting Higher-order Stack Trees

In this talk, I will present the model of stack tree rewriting systems, as a common extension of higher-order pushdown automata and ground tree rewriting system. I will define the model of stack trees, the operations I allow on them, and an automaton model to accept regular sets of operations. I will show that for the graphs generated by this model, the model-checking problem for FO[->*] is decidable.