Abstract

Ground Tree Rewrite Systems with State provide a model of tree-manipulating programs and may be used as an abstraction of first-order recursive programs with dynamic thread creation. Unfortunately such systems are known to have an undecidable control state reachability problem.

The same undecidability holds also for two-threaded recursive programs, leading to the study of under-approximation techniques such as context-bounding, and, more recently, scope-bounding. In this talk we will look at the transfer of these under-approximations to ground tree rewrite systems with state, in particular leading to the introduction of Senescent Ground Tree Rewrite Systems.

Senescent ground tree rewrite systems 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. That is, the tree is subject to the effects of aging where the passage of time is marked by the control state.

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 was presented at CSL -LICS 2014.