License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2015.368
URN: urn:nbn:de:0030-drops-53899
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5389/
Go to the corresponding LIPIcs Volume Portal

Fisman, Dana ; Lustig, Yoad

A Modular Approach for Büchi Determinization

pdf-format:
29.pdf (0.6 MB)

Abstract

The problem of Büchi determinization is a fundamental problem with important applications in reactive synthesis, multi-agent systems and probabilistic verification. The first asymptotically optimal Büchi determinization (a.k.a the Safra construction), was published in 1988. While asymptotically optimal, the Safra construction is notorious for its technical complexity and opaqueness in terms of intuition. While some improvements were published since the Safra construction, notably Kähler and Wilke’s construction, understanding the constructions remains a non-trivial task.

In this paper we present a modular approach to Büchi determinization, where the difficulties are addressed one at a time, rather than simultaneously, making the solutions natural and easy to understand. We build on the notion of the skeleton trees of Kähler and Wilke. We first show how to construct a deterministic automaton in the case the skeleton's width is one. Then we show how to construct a deterministic automaton in the case the skeleton's width is k (for any given k). The overall construction is obtained by running in parallel the automata for all widths.

BibTeX - Entry

@InProceedings{fisman_et_al:LIPIcs:2015:5389,
  author =	{Dana Fisman and Yoad Lustig},
  title =	{{A Modular Approach for B{\"u}chi Determinization}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{368--382},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Luca Aceto and David de Frutos Escrig},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5389},
  URN =		{urn:nbn:de:0030-drops-53899},
  doi =		{10.4230/LIPIcs.CONCUR.2015.368},
  annote =	{Keywords: B{\"u}chi automata, Determinization, Verification, Games, Synthesis}
}

Keywords: Büchi automata, Determinization, Verification, Games, Synthesis
Collection: 26th International Conference on Concurrency Theory (CONCUR 2015)
Issue Date: 2015
Date of publication: 26.08.2015

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI