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

  Browse A-Z

Log in

University Account External (via Google)

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹī¸ Information

Infinite-State System Verification via Tree Automata

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.

This talk is included in these lists:

Note that ex-directory lists are not shown.

Other lists

Economic and Social History Seminars Branching Out Talk Series University Centre (Mill Lane)

Other talks

TBC Title to be confirmed title abstract tba Argentina 2005 Title to be confirmed Cambridge RNA Club - ONLINE
 

Š 2006-2025 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity