Product of Parity Automata

Authors

Laurent Xu

Type

techreport

Year

2016

Number

1607

Abstract

Spot, a library for transition based Spot, a library for transition-based $\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.