Document Open Access Logo

A Hierarchy of Nondeterminism

Authors Bader Abu Radi, Orna Kupferman, Ofer Leshkowitz

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2021.85.pdf
  • Filesize: 0.73 MB
  • 21 pages

Document Identifiers

Author Details

Bader Abu Radi
  • School of Engineering and Computer Science, Hebrew University, Jerusalem, Israel
Orna Kupferman
  • School of Engineering and Computer Science, Hebrew University, Jerusalem, Israel
Ofer Leshkowitz
  • School of Engineering and Computer Science, Hebrew University, Jerusalem, Israel

Cite AsGet BibTex

Bader Abu Radi, Orna Kupferman, and Ofer Leshkowitz. A Hierarchy of Nondeterminism. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 85:1-85:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.MFCS.2021.85

Abstract

We study three levels in a hierarchy of nondeterminism: A nondeterministic automaton A is determinizable by pruning (DBP) if we can obtain a deterministic automaton equivalent to A by removing some of its transitions. Then, A is good-for-games (GFG) if its nondeterministic choices can be resolved in a way that only depends on the past. Finally, A is semantically deterministic (SD) if different nondeterministic choices in A lead to equivalent states. Some applications of automata in formal methods require deterministic automata, yet in fact can use automata with some level of nondeterminism. For example, DBP automata are useful in the analysis of online algorithms, and GFG automata are useful in synthesis and control. For automata on finite words, the three levels in the hierarchy coincide. We study the hierarchy for Büchi, co-Büchi, and weak automata on infinite words. We show that the hierarchy is strict, study the expressive power of the different levels in it, as well as the complexity of deciding the membership of a language in a given level. Finally, we describe a probability-based analysis of the hierarchy, which relates the level of nondeterminism with the probability that a random run on a word in the language is accepting.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automata over infinite objects
Keywords
  • Automata on Infinite Words
  • Expressive power
  • Complexity
  • Games

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. B. Alpern and F.B. Schneider. Recognizing safety and liveness. Distributed computing, 2:117-126, 1987. Google Scholar
  2. B. Aminof, O. Kupferman, and R. Lampert. Reasoning about online algorithms with weighted automata. ACM Transactions on Algorithms, 6(2), 2010. Google Scholar
  3. G. Avni and O. Kupferman. Stochastization of weighted automata. In 40th Int. Symp. on Mathematical Foundations of Computer Science, volume 9234 of Lecture Notes in Computer Science, pages 89-102. Springer, 2015. Google Scholar
  4. M. Bagnol and D. Kuperberg. Büchi good-for-games automata are efficiently recognizable. In Proc. 38th Conf. on Foundations of Software Technology and Theoretical Computer Science, volume 122 of LIPIcs, pages 16:1-16:14. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2018. Google Scholar
  5. U. Boker, D. Kuperberg, O. Kupferman, and M. Skrzypczak. Nondeterminism in the presence of a diverse or unknown future. In Proc. 40th Int. Colloq. on Automata, Languages, and Programming, volume 7966 of Lecture Notes in Computer Science, pages 89-100, 2013. Google Scholar
  6. U. Boker, D. Kuperberg, K. Lehtinen, and M. Skrzypczak. On the succinctness of alternating parity good-for-games automata. In Proc. 40th Conf. on Foundations of Software Technology and Theoretical Computer Science, volume 182 of LIPIcs, pages 41:1-41:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. Google Scholar
  7. U. Boker, O. Kupferman, and M. Skrzypczak. How deterministic are Good-For-Games automata? In Proc. 37th Conf. on Foundations of Software Technology and Theoretical Computer Science, volume 93 of Leibniz International Proceedings in Informatics (LIPIcs), pages 18:1-18:14, 2017. Google Scholar
  8. U. Boker and K. Lehtinen. Good for games automata: From nondeterminism to alternation. In Proc. 30th Int. Conf. on Concurrency Theory, volume 140 of LIPIcs, pages 19:1-19:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. Google Scholar
  9. J.R. Büchi. On a decision method in restricted second order arithmetic. In Proc. Int. Congress on Logic, Method, and Philosophy of Science. 1960, pages 1-12. Stanford University Press, 1962. Google Scholar
  10. K. Chatterjee, M. Jurdziński, and T.A. Henzinger. Simple stochastic parity games. In Proc. 12th Annual Conf. of the European Association for Computer Science Logic, volume 2803, pages 100-113. Springer, 2003. Google Scholar
  11. Th. Colcombet. The theory of stabilisation monoids and regular cost functions. In Proc. 36th Int. Colloq. on Automata, Languages, and Programming, volume 5556 of Lecture Notes in Computer Science, pages 139-150. Springer, 2009. Google Scholar
  12. T.A. Henzinger and N. Piterman. Solving games without determinization. In Proc. 15th Annual Conf. of the European Association for Computer Science Logic, volume 4207 of Lecture Notes in Computer Science, pages 394-410. Springer, 2006. Google Scholar
  13. D. Kuperberg and A. Majumdar. Width of non-deterministic automata. In Proc. 35th Symp. on Theoretical Aspects of Computer Science, volume 96 of LIPIcs, pages 47:1-47:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. Google Scholar
  14. D. Kuperberg and M. Skrzypczak. On determinisation of good-for-games automata. In Proc. 42nd Int. Colloq. on Automata, Languages, and Programming, pages 299-310, 2015. Google Scholar
  15. O. Kupferman. Automata theory and model checking. In Handbook of Model Checking, pages 107-151. Springer, 2018. Google Scholar
  16. O. Kupferman, S. Safra, and M.Y. Vardi. Relating word and tree automata. Ann. Pure Appl. Logic, 138(1-3):126-146, 2006. Google Scholar
  17. O. Kupferman and M.Y. Vardi. From linear time to branching time. ACM Transactions on Computational Logic, 6(2):273-294, 2005. Google Scholar
  18. O. Kupferman and M.Y. Vardi. Safraless decision procedures. In Proc. 46th IEEE Symp. on Foundations of Computer Science, pages 531-540, 2005. Google Scholar
  19. L.H. Landweber. Decision problems for ω-automata. Mathematical Systems Theory, 3:376-384, 1969. Google Scholar
  20. K. Lehtinen and M. Zimmermann. Good-for-games ω-pushdown automata. In Proc. 35th IEEE Symp. on Logic in Computer Science, 2020. Google Scholar
  21. S. Miyano and T. Hayashi. Alternating finite automata on ω-words. Theoretical Computer Science, 32:321-330, 1984. Google Scholar
  22. G. Morgenstern. Expressiveness results at the bottom of the ω-regular hierarchy. M.Sc. Thesis, The Hebrew University, 2003. Google Scholar
  23. D.E. Muller, A. Saoudi, and P. E. Schupp. Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential time. In Proc. 3rd IEEE Symp. on Logic in Computer Science, pages 422-427, 1988. Google Scholar
  24. D. Niwinski and I. Walukiewicz. Relating hierarchies of word and tree automata. In Proc. 15th Symp. on Theoretical Aspects of Computer Science, volume 1373 of Lecture Notes in Computer Science. Springer, 1998. Google Scholar
  25. M.O. Rabin and D. Scott. Finite automata and their decision problems. IBM Journal of Research and Development, 3:115-125, 1959. Google Scholar
  26. S. Safra. On the complexity of ω-automata. In Proc. 29th IEEE Symp. on Foundations of Computer Science, pages 319-327, 1988. Google Scholar
  27. A.P. Sistla. Safety, liveness and fairness in temporal logic. Formal Aspects of Computing, 6:495-511, 1994. Google Scholar
  28. A.P. Sistla, M.Y. Vardi, and P. Wolper. The complementation problem for Büchi automata with applications to temporal logic. Theoretical Computer Science, 49:217-237, 1987. Google Scholar
  29. M.Y. Vardi and P. Wolper. Reasoning about infinite computations. Information and Computation, 115(1):1-37, 1994. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact