Deciding weak definability for Büchi definable tree languages

Michael Vanden Boom

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.