University of Cambridge > > Logic and Semantics Seminar (Computer Laboratory) > Infinite-State System Verification via Tree Automata

Infinite-State System Verification via Tree Automata

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

  • UserWolfgang Thomas, RWTH Aachen
  • ClockFriday 11 May 2007, 14:00-15:00
  • HouseFW11.

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


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