BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Senescent Ground Tree Rewrite Systems - Matthew Hague\, Royal Holl
 oway
DTSTART:20141121T160000Z
DTEND:20141121T170000Z
UID:TALK55911@talks.cam.ac.uk
CONTACT:Jonathan Hayman
DESCRIPTION:Ground Tree Rewrite Systems with State provide a model of tree
 -manipulating programs and may be used as an abstraction of first-order re
 cursive programs with dynamic thread creation.  Unfortunately such systems
  are known to have an undecidable control state reachability problem.\n\n\
 nThe same undecidability holds also for two-threaded recursive programs\, 
 leading to the study of under-approximation techniques such as context-bou
 nding\, and\, more recently\, scope-bounding.  In this talk we will look a
 t the transfer of these under-approximations to ground tree rewrite system
 s with state\, in particular leading to the introduction of Senescent Grou
 nd Tree Rewrite Systems.\n\n\nSenescent ground tree rewrite systems are a 
 restriction of ground tree rewrite systems with state such that nodes of t
 he tree may no longer be rewritten after having witnessed an a priori fixe
 d number of control state changes.  That is\, the tree is subject to the e
 ffects of aging where the passage of time is marked by the control state. 
 \n\n\nAs well as generalising scope-bounded multi-stack pushdown systems\,
  we show - via reductions to and from reset Petri-nets - that these system
 s have an Ackermann-complete control state reachability problem.  However\
 , reachability of a regular set of trees remains undecidable. \n\n\nThis w
 ork was presented at CSL-LICS 2014.
LOCATION:Room FW26\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR