Parity and generalised Büchi automata - determinisation and complementation

Methrayil Varghese, Praveen Thomas Parity and generalised Büchi automata - determinisation and complementation. PhD thesis, University of Liverpool.

	Text Methrayil-VarghesePra_Nov2014_2027479.pdf - Author Accepted Manuscript Available under License Creative Commons Attribution. Download (735kB)
	Text (Blank) Title - Unspecified Access to this file is embargoed until Unspecified. Available under License Creative Commons Attribution. Download (77B)

Abstract

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 Büchi automata and nondeterministic parity automata. Generalised Büchi and parity automata occur naturally in model-checking, realisability checking and synthesis procedures. We first review a tight determinisation procedure for Büchi automata, which uses a simplification of Safra trees called history trees. As Büchi automata are special types of both generalised Büchi and parity automata, we adjust the data structure to arrive at suitably tight determinisation constructions for both generalised Büchi and parity automata. As the parity condition describes combinations of Büchi and CoBüchi 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 Büchi determinisation: we then nest these structures to reflect the standard parity condition and describe a direct determinisation construction. The generalised Büchi condition is characterised by an accepting family with 'k' accepting sets. It is easy to extend classic determinisation constructions to handle generalised Büchi automata by incorporating the degeneralization algorithm in the determinisation construction. We extend the tight Büchi 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 Büchi and 1-pair Rabin. We also reconnect tight determinisation and complementation and provide constructions for complementing generalised Büchi 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.

Item Type:	Thesis (PhD)
Additional Information:	Date: 2014-11 (completed)
Subjects:	?? QA75 ??
Depositing User:	Symplectic Admin
Date Deposited:	01 Feb 2016 15:23
Last Modified:	16 Dec 2022 04:43
DOI:	10.17638/02027479
URI:	https://livrepository.liverpool.ac.uk/id/eprint/2027479