University of Cambridge > > Logic and Semantics Seminar (Computer Laboratory) > Senescent Ground Tree Rewrite Systems

Senescent Ground Tree Rewrite Systems

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Jonathan Hayman.

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.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2022, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity