A Hierarchy of Nondeterminism
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.
Automata on Infinite Words
Expressive power
Complexity
Games
Theory of computation~Automata over infinite objects
85:1-85:21
Regular Paper
Bader
Abu Radi
Bader Abu Radi
School of Engineering and Computer Science, Hebrew University, Jerusalem, Israel
Orna
Kupferman
Orna Kupferman
School of Engineering and Computer Science, Hebrew University, Jerusalem, Israel
Ofer
Leshkowitz
Ofer Leshkowitz
School of Engineering and Computer Science, Hebrew University, Jerusalem, Israel
10.4230/LIPIcs.MFCS.2021.85
B. Alpern and F.B. Schneider. Recognizing safety and liveness. Distributed computing, 2:117-126, 1987.
B. Aminof, O. Kupferman, and R. Lampert. Reasoning about online algorithms with weighted automata. ACM Transactions on Algorithms, 6(2), 2010.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
O. Kupferman. Automata theory and model checking. In Handbook of Model Checking, pages 107-151. Springer, 2018.
O. Kupferman, S. Safra, and M.Y. Vardi. Relating word and tree automata. Ann. Pure Appl. Logic, 138(1-3):126-146, 2006.
O. Kupferman and M.Y. Vardi. From linear time to branching time. ACM Transactions on Computational Logic, 6(2):273-294, 2005.
O. Kupferman and M.Y. Vardi. Safraless decision procedures. In Proc. 46th IEEE Symp. on Foundations of Computer Science, pages 531-540, 2005.
L.H. Landweber. Decision problems for ω-automata. Mathematical Systems Theory, 3:376-384, 1969.
K. Lehtinen and M. Zimmermann. Good-for-games ω-pushdown automata. In Proc. 35th IEEE Symp. on Logic in Computer Science, 2020.
S. Miyano and T. Hayashi. Alternating finite automata on ω-words. Theoretical Computer Science, 32:321-330, 1984.
G. Morgenstern. Expressiveness results at the bottom of the ω-regular hierarchy. M.Sc. Thesis, The Hebrew University, 2003.
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.
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.
M.O. Rabin and D. Scott. Finite automata and their decision problems. IBM Journal of Research and Development, 3:115-125, 1959.
S. Safra. On the complexity of ω-automata. In Proc. 29th IEEE Symp. on Foundations of Computer Science, pages 319-327, 1988.
A.P. Sistla. Safety, liveness and fairness in temporal logic. Formal Aspects of Computing, 6:495-511, 1994.
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.
M.Y. Vardi and P. Wolper. Reasoning about infinite computations. Information and Computation, 115(1):1-37, 1994.
Bader Abu Radi, Orna Kupferman, and Ofer Leshkowitz
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode