InfiniteState System Verification via Tree Automata
Add to your list(s)
Download to your calendar using vCal
 Wolfgang Thomas, RWTH Aachen
 Friday 11 May 2007, 14:0015:00
 FW11.
If you have a question about this talk, please contact Tom Ridge.
A standard approach in “infinitestate modelchecking” is the
representation of infinite transition systems by rewriting
systems over words. A wellknown example is given by the class
of pushdown systems, where prefix rewriting is applied and
stateproperties are presented as regular sets of words. In
this talk, we report on a more general approach, pursued in
Aachen in recent years, in which trees, ground tree rewriting,
and regular tree languages are considered instead. It turns out
that a considerably larger class of transition systems is
generated for which, e.g., the reachability problem is still
efficiently decidable. We also show that undecidability phenomena
arise when passing to more complex specifications than reachability.
We conclude with an outline of open problems.
This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.
This talk is included in these lists:
Note that exdirectory lists are not shown.
