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.