Skip to main content
School of Electronic Engineering and Computer Science

Seminar: Michael Vanden Boom

13 November 2013

Time: 11:30am - 12:30pm
Venue: CS 414 4th Floor, Computer Science Bldg Queen Mary, University of London Mile End London E1 4NS

Theory Seminar: Deciding weak definability for Büchi definable tree languages

Michael Vanden Boom (Oxford))
Host: Nikos Tzevelekos

Deciding weak definability for Büchi definable tree languages

Michael Vanden Boom (Oxford)

Weakly definable languages of infinite trees are an expressive subclass of regular tree languages definable in terms of weak monadic second-order logic, or equivalently weak alternating automata. These languages subsume temporal logics like CTL, but still admit efficient (linear time) model checking.

In this talk, I describe the problem of determining whether a given language is weakly definable. In particular, I present recent work showing that given a Büchi automaton as input, it is decidable whether the language is weakly definable. The proof is by reduction to a boundedness problem for cost automata (a form of automata with counters).

Joint work with Thomas Colcombet, Denis Kuperberg, and Christof Löding.

Back to top