BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Infinite-State System Verification via Tree Automata - Wolfgang Th
 omas\, RWTH Aachen
DTSTART:20070511T130000Z
DTEND:20070511T140000Z
UID:TALK6955@talks.cam.ac.uk
CONTACT:Tom Ridge
DESCRIPTION:A standard approach in "infinite-state model-checking" is the\
 nrepresentation of infinite transition systems by rewriting\nsystems over 
 words. A well-known example is given by the class\nof pushdown systems\, w
 here prefix rewriting is applied and\nstate-properties are presented as re
 gular sets of words. In\nthis talk\, we report on a more general approach\
 , pursued in\nAachen in recent years\, in which trees\, ground tree rewrit
 ing\,\nand regular tree languages are considered instead. It turns out\nth
 at a considerably larger class of transition systems is\ngenerated for whi
 ch\, e.g.\, the reachability problem is still\nefficiently decidable. We a
 lso show that undecidability phenomena\narise when passing to more complex
  specifications than reachability.\nWe conclude with an outline of open pr
 oblems.
LOCATION:FW11
END:VEVENT
END:VCALENDAR