License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ICALP.2023.109
URN: urn:nbn:de:0030-drops-181610
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18161/
Go to the corresponding LIPIcs Volume Portal

Abu Radi, Bader ; Kupferman, Orna

On Semantically-Deterministic Automata

pdf-format:
LIPIcs-ICALP-2023-109.pdf (0.8 MB)

Abstract

Nondeterminism is a fundamental notion in Theoretical Computer Science. A nondeterministic automaton is semantically deterministic (SD) if different nondeterministic choices in the automaton lead to equivalent states. Semantic determinism is interesting as it is a natural relaxation of determinism, and as some applications of automata in formal methods require deterministic automata, yet in fact can use automata with some level of nondeterminism, tightly related to semantic determinism.
In the context of finite words, semantic determinism coincides with determinism, in the sense that every pruning of an SD automaton to a deterministic one results in an equivalent automaton. We study SD automata on infinite words, focusing on Büchi, co-Büchi, and weak automata. We show that there, while semantic determinism does not increase the expressive power, the combinatorial and computational properties of SD automata are very different from these of deterministic automata. In particular, SD Büchi and co-Büchi automata are exponentially more succinct than deterministic ones (in fact, also exponentially more succinct than history-deterministic automata), their complementation involves an exponential blow up, and decision procedures for them like universality and minimization are PSPACE-complete. For weak automata, we show that while an SD weak automaton need not be pruned to an equivalent deterministic one, it can be determinized to an equivalent deterministic weak automaton with the same state space, implying also efficient complementation and decision procedures for SD weak automata.

BibTeX - Entry

@InProceedings{aburadi_et_al:LIPIcs.ICALP.2023.109,
  author =	{Abu Radi, Bader and Kupferman, Orna},
  title =	{{On Semantically-Deterministic Automata}},
  booktitle =	{50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)},
  pages =	{109:1--109:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-278-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{261},
  editor =	{Etessami, Kousha and Feige, Uriel and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2023/18161},
  URN =		{urn:nbn:de:0030-drops-181610},
  doi =		{10.4230/LIPIcs.ICALP.2023.109},
  annote =	{Keywords: Automata on infinite words, Nondeterminism, Succinctness, Decision procedures}
}

Keywords: Automata on infinite words, Nondeterminism, Succinctness, Decision procedures
Collection: 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)
Issue Date: 2023
Date of publication: 05.07.2023

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