Product of Parity Automata

From LRDE

Abstract

Spot, a library for transition based Spot, a library for transition-based Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \omega} -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.