Time: 11:30am - 12:30pm Venue: CS 414 4th Floor, Computer Science Bldg Queen Mary, University of London Mile End London E1 4NS
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.