Parity and generalised Büchi automata : determinisation and complementation
Methrayil Varghese, Praveen Thomas · 2014
In this thesis, we study the problems of determinisation and complementation of finite automata on infinite words. We focus on two classes of automata that occur naturally: generalised Buchi automata and nondeterministic parity automata. Generalised Buchi and parity automata occur naturally in model-checking, realisability checking and synthesis procedures. We first review a tight determinisation procedure for Buchi automata, which uses a simplification of Safra trees called history trees. As Buchi automata are special types of both generalised Buchi and parity automata, we adjust the data structure to arrive at suitably tight determinisation constructions for both generalised Buchi and parity automata. As the parity condition describes combinations of Buchi and CoBuchi conditions, instead of immediately modifying the data structure to handle parity automata, we arrive at a suitable data structure by first looking at a special case, Rabin automata with one accepting pair. One pair Rabin automata correspond to parity automata with three priorities and serve as a starting point to modify the structures that result from Buchi determinisation: we then nest these structures to reflect the standard parity condition and describe a direct determinisation construction. The generalised Buchi condition is characterised by an accepting family with 'k' accepting sets. It is easy to extend classic determinisation constructions to handle generalised Buchi automata by incorporating the degeneralization algorithm in the determinisation construction. We extend the tight Buchi construction to do exactly this. Our determinisation constructions go to deterministic Rabin automata. It is known that one can determinise to the more convenient parity condition by incorporating the standard Latest Appearance Record construction in the determinisation procedure. We determinise to parity automata using this technique. We prove lower bounds on these constructions. In the case of determinisation to Rabin automata, our constructions are tight to the state. In the case of determinisation to parity, there is a constant factor ≤ 1.5 between upper and lower bounds reducing to optimal(to the state) in the case of Buchi and 1-pair Rabin. We also reconnect tight determinisation and complementation and provide constructions for complementing generalised Buchi and parity automata by starting withour data structure for determinisation. We introduce suitable data structures for the complementation procedures based on the data structure used for determinisation. We prove lower bounds for both constructions that are tight upto an O(n) factor where 'n' is the number of states of the nondeterministic automaton that is complemented.