Please use this identifier to cite or link to this item:
Title: From nondeterministic Buchi and Streett automata to deterministic parity automata
Authors: Piterman, Nir
First Published: 14-Aug-2007
Presented at: 21st Annual IEEE Symposium on Logic in Computer Science (LICS 2006), Seattle, WA
Start Date: 12-Aug-2006
End Date: 15-Aug-2006
Publisher: IEEE
Citation: 21st annual IEEE symposium on logic in computer science, proceedings, 2006, pp. 255-264
Abstract: In this paper we revisit Safra's determinization constructions. We show how to construct deterministic automata with fewer states and, most importantly, parity acceptance conditions. Specifically, starting from a nondeterministic Buchi automaton with n states our construction yields a deterministic parity automaton with n2n+2 states and index 2n (instead of a Rabin automaton with (12)nn2n states and n pairs). Starting from a nondeterministic Streett automaton with n states and k pairs our construction yields a deterministic parity automaton with nn(k+2)+2(k+1)2n(K+1) states and index 2n(k+1) (instead of a Rabin automaton with (12)n(k+1)n n(k+2)(k+1)2n(k+1) states and n(k+1) pairs). The parity condition is much simpler than the Rabin condition. In applications such as solving games and emptiness of tree automata handling the Rabin condition involves an additional multiplier of n2n!(or(n(k+1))2(n(k+1))! in the case of Streett) which is saved using our construction.
DOI Link: 10.1109/LICS.2006.28
ISSN: 1043-6871
ISBN: 0-7695-2631-4
Version: Publisher Version
Status: Peer-reviewed
Type: Conference Paper
Rights: Copyright © the authors, 2007. This is an Open Access article distributed under the terms of the Creative Commons Attribution NoDerivs Licence ( )
Appears in Collections:Conference Papers & Presentations, Dept. of Computer Science

Files in This Item:
File Description SizeFormat 
0705.2205v2.pdfPlease select a version289.97 kBAdobe PDFView/Open

Items in LRA are protected by copyright, with all rights reserved, unless otherwise indicated.