Infinite-State 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:00-15:00
• FW11.

If you have a question about this talk, please contact Tom Ridge.

A standard approach in “infinite-state model-checking” is the representation of infinite transition systems by rewriting systems over words. A well-known example is given by the class of pushdown systems, where prefix rewriting is applied and state-properties 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:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• FW11
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• tcw57’s list
• yk373's list

Note that ex-directory lists are not shown.