Senescent Ground Tree Rewrite Systems

Ground Tree Rewrite Systems with State are known to have an undecidable control state reachability problem. Taking inspiration from the recent introduction of scope-bounded multi-stack pushdown systems, we define Senescent Ground Tree Rewrite Systems. These are a restriction of ground tree rewrite systems with state such that nodes of the tree may no longer be rewritten after having witnessed an a priori fixed number of control state changes. As well as generalising scope-bounded multi-stack pushdown systems, we show - via reductions to and from reset Petri-nets - that these systems have an Ackermann-complete control state reachability problem. However, reachability of a regular set of trees remains undecidable. This work is to appear in CSL-LICS 2014.

Authors

• Matthew Hague

Keywords

No keywords are indexed for this paper.