Automata transformations

In the world of automata, there is a trade-off between how concisely an automaton can represent a property and the complexity of checking for membership and emptiness. Büchi and Weak automata allow for simpler algorithms than more complex automata types, but are often larger. The trade-offs between different automata types are poorly understood, and, I believe, instrumental to algorithmic issues such as the complexity of solving parity games. The blow-up of transformations into simple automata, such as Weak or Büchi automata is a way to capture this trade-off.

I’ve worked on two transformations from alternating parity automata to alternating weak automata: one based on register games with Udi Boker, and one based on progress measures and universal trees with Marcin Jurdziński and Laure Daviaud. The paper with Udi also includes a lower bound that shows that on trees Büchi automata are not only more expressive, but also exponentially more concise than weak automata.