Menu

School of Electronic Engineering and Computer Science

events menu
Nov 13

Seminar: Michael Vanden Boom

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.

Wed 13th November 2013

Start Time: 11:30
End Time: 12:30

 

CS 414
4th Floor, Computer Science Bldg
Queen Mary, University of London
Mile End
London
E1 4NS

Return to top