Résumé | In this talk, I will present a construction that takes as input a Muller automaton and transforms it into a parity automaton in an optimal way. More precisely, the resulting parity automaton has minimal size and uses a minimal number of priorities among those automata that admit a locally bijective morphism to the original Muller automaton. This transformation and the optimality result can also be applied to games and other types of transition systems.
We show two applications: an improvement on the determinisation of Büchi automata into deterministic parity automata, and a new proof of the fact that a Muller automaton can be labelled with a parity condition iff it can be labelled with both a Rabin and a Sttreet condition (recognizing the same language).
This work was done during my master's internship at the IRIF with Thomas Colcombet and Nathanaël Fijalkow. |