DROPS

Document

Track B: Automata, Logic, Semantics, and Theory of Programming

DOI: 10.4230/LIPIcs.ICALP.2019.120

Determinization of Büchi Automata: Unifying the Approaches of Safra and Muller-Schupp (Track B: Automata, Logic, Semantics, and Theory of Programming)

Authors: Christof Löding and Anton Pirogov

Published in: LIPIcs, Volume 132, 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)

Abstract

Determinization of Büchi automata is a long-known difficult problem, and after the seminal result of Safra, who developed the first asymptotically optimal construction from Büchi into Rabin automata, much work went into improving, simplifying, or avoiding Safra’s construction. A different, less known determinization construction was proposed by Muller and Schupp. The two types of constructions share some similarities but their precise relationship was still unclear. In this paper, we shed some light on this relationship by proposing a construction from nondeterministic Büchi to deterministic parity automata that subsumes both constructions: Our construction leaves some freedom in the choice of the successor states of the deterministic automaton, and by instantiating these choices in different ways, one obtains as particular cases the construction of Safra and the construction of Muller and Schupp. The basis is a correspondence between structures that are encoded in the macrostates of the determinization procedures - Safra trees on one hand, and levels of the split-tree, which underlies the Muller and Schupp construction, on the other hand. Our construction also allows for mixing the mentioned constructions, and opens up new directions for the development of heuristics.

Cite as

Christof Löding and Anton Pirogov. Determinization of Büchi Automata: Unifying the Approaches of Safra and Muller-Schupp (Track B: Automata, Logic, Semantics, and Theory of Programming). In 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 132, pp. 120:1-120:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{loding_et_al:LIPIcs.ICALP.2019.120,
  author =	{L\"{o}ding, Christof and Pirogov, Anton},
  title =	{{Determinization of B\"{u}chi Automata: Unifying the Approaches of Safra and Muller-Schupp}},
  booktitle =	{46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)},
  pages =	{120:1--120:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-109-2},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{132},
  editor =	{Baier, Christel and Chatzigiannakis, Ioannis and Flocchini, Paola and Leonardi, Stefano},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2019.120},
  URN =		{urn:nbn:de:0030-drops-106963},
  doi =		{10.4230/LIPIcs.ICALP.2019.120},
  annote =	{Keywords: B\"{u}chi automata, determinization, parity automata}
}

Search Results

Documents authored by Pirogov, Anton

Determinization of Büchi Automata: Unifying the Approaches of Safra and Muller-Schupp (Track B: Automata, Logic, Semantics, and Theory of Programming)

Abstract

Cite as

Thanks for your feedback!

Could not send message