Product of Parity Automata



Spot, a library for transition based Spot, a library for transition-based -automata manipulation, provides a method to determinize Büchi automata which can produce quasi-parity automata. We introduce three tools to manipulate these automata which are reducing the number of sets in the acceptance condition, changing the style of the parity acceptance expression and colorizing an automaton. Olivier Carton introduced a method to construct the product of state-based parity automata which keeps the parity acceptance. We adapt this method to make it work with transition-based automata and we present optimizations of this product. Our work gives a better support of automata with parity acceptance and may also lead to further optimizations of the determinization of Büchi automata.