Document Open Access Logo

On Semantically-Deterministic Automata

Authors Bader Abu Radi , Orna Kupferman

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2023.109.pdf
  • Filesize: 0.75 MB
  • 20 pages

Document Identifiers

Author Details

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

Funding

This research is supported by the Israel Science Foundation, Grant 2357/19, the European Research Council, Advanced Grant ADVANSYNT, and the Neubauer Foundation of Ph.D Fellowship.

Cite AsGet BibTex

Bader Abu Radi and Orna Kupferman. On Semantically-Deterministic Automata. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 109:1-109:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.ICALP.2023.109

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Formal languages and automata theory
Keywords
  • Automata on infinite words
  • Nondeterminism
  • Succinctness
  • Decision procedures

Metrics

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

Related Versions

References

  1. B. Abu Radi and O. Kupferman. Minimizing GFG transition-based automata. In Proc. 46th Int. Colloq. on Automata, Languages, and Programming, volume 132 of LIPIcs, pages 100:1-100:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. Google Scholar
  2. B. Abu Radi and O. Kupferman. On semantically-deterministic automata. CoRR, abs/2305.15489, 2023. URL: https://arxiv.org/abs/2305.15489.
  3. B. Abu Radi, O. Kupferman, and O. Leshkowitz. A hierarchy of nondeterminism. In 46th Int. Symp. on Mathematical Foundations of Computer Science, volume 202 of LIPIcs, pages 85:1-85:21, 2021. Google Scholar
  4. B. Aminof, O. Kupferman, and R. Lampert. Reasoning about online algorithms with weighted automata. ACM Transactions on Algorithms, 6(2), 2010. Google Scholar
  5. 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, 2018. Google Scholar
  6. B. Boigelot, S. Jodogne, and P. Wolper. On the use of weak automata for deciding linear arithmetic with integer and real variables. In Proc. Int. Joint Conf. on Automated Reasoning, volume 2083 of Lecture Notes in Computer Science, pages 611-625. Springer, 2001. Google Scholar
  7. 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
  8. U. Boker and K. Lehtinen. When a little nondeterminism goes a long way: an introduction to history-determinism. ACM SIGLOG News, 10(1):177-196, 2023. 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. Olivier Carton and Max Michel. Unambiguous büchi automata. Theoretical Computer Science, 297(1):37-81, 2003. Google Scholar
  11. T. 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. Colcombet, K. Quaas, and M. Skrzypczak. Unambiguity in automata theory (dagstuhl seminar 21452). Dagstuhl Reports, 11(10):57-71, 2021. Google Scholar
  13. A. Duret-Lutz, A. Lewkowicz, A. Fauchille, Th. Michaud, E. Renault, and L. Xu. Spot 2.0 - a framework for LTL and ω-automata manipulation. In 14th Int. Symp. on Automated Technology for Verification and Analysis, volume 9938 of Lecture Notes in Computer Science, pages 122-129. Springer, 2016. Google Scholar
  14. P. Gastin and D. Oddoux. Fast LTL to Büchi automata translation. In Proc. 13th Int. Conf. on Computer Aided Verification, volume 2102 of Lecture Notes in Computer Science, pages 53-65. Springer, 2001. Google Scholar
  15. D. Giannakopoulou and F. Lerda. From states to transitions: Improving translation of LTL formulae to Büchi automata. In Proc. 22nd International Conference on Formal Techniques for Networked and Distributed Systems, volume 2529 of Lecture Notes in Computer Science, pages 308-326. Springer, 2002. Google Scholar
  16. E.M. Hahn, M. Perez, S. Schewe, F. Somenzi, A. Trivedi, and D. Wojtczak. Good-for-MDPs automata for probabilistic analysis and reinforcement learning. In Proc. 26th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, volume 12078 of Lecture Notes in Computer Science, pages 306-323. Springer, 2020. Google Scholar
  17. T.A. Henzinger, O. Kupferman, and S. Rajamani. Fair simulation. Information and Computation, 173(1):64-81, 2002. Google Scholar
  18. 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
  19. T. Jiang and B. Ravikumar. Minimal NFA problems are hard. SIAM Journal on Computing, 22(6):1117-1141, 1993. Google Scholar
  20. 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
  21. O. Kupferman. Avoiding determinization. In Proc. 21st IEEE Symp. on Logic in Computer Science, pages 243-254, 2006. Google Scholar
  22. O. Kupferman. Automata theory and model checking. In Handbook of Model Checking, pages 107-151. Springer, 2018. Google Scholar
  23. O. Kupferman. Using the past for resolving the future. Frontiers in Computer Science, 4, 2023. Google Scholar
  24. O. Kupferman and O. Leshkowitz. On repetition languages. In 45th Int. Symp. on Mathematical Foundations of Computer Science, Leibniz International Proceedings in Informatics (LIPIcs), 2020. Google Scholar
  25. 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
  26. 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
  27. R.P. Kurshan. Complementing deterministic Büchi automata in polynomial time. Journal of Computer and Systems Science, 35:59-71, 1987. Google Scholar
  28. R.P. Kurshan. Computer Aided Verification of Coordinating Processes. Princeton Univ. Press, 1994. Google Scholar
  29. L.H. Landweber. Decision problems for ω-automata. Mathematical Systems Theory, 3:376-384, 1969. Google Scholar
  30. W. Li, Sh. Kan, and Z. Huang. A better translation from LTL to transition-based generalized Büchi automata. IEEE Access, 5:27081-27090, 2017. Google Scholar
  31. C. Löding. Efficient minimization of deterministic weak ω-automata. Information Processing Letters, 79(3):105-109, 2001. Google Scholar
  32. S. Miyano and T. Hayashi. Alternating finite automata on ω-words. Theoretical Computer Science, 32:321-330, 1984. Google Scholar
  33. G. Morgenstern. Expressiveness results at the bottom of the ω-regular hierarchy. M.Sc. Thesis, The Hebrew University, 2003. Google Scholar
  34. 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
  35. M.O. Rabin and D. Scott. Finite automata and their decision problems. IBM Journal of Research and Development, 3:115-125, 1959. Google Scholar
  36. S. Safra. On the complexity of ω-automata. In Proc. 29th IEEE Symp. on Foundations of Computer Science, pages 319-327, 1988. Google Scholar
  37. S. Schewe. Beyond Hyper-Minimisation - Minimising DBAs and DPAs is NP-Complete. In Proc. 30th Conf. on Foundations of Software Technology and Theoretical Computer Science, volume 8 of Leibniz International Proceedings in Informatics (LIPIcs), pages 400-411, 2010. Google Scholar
  38. S. Schewe. Minimising good-for-games automata is NP-complete. In Proc. 40th Conf. on Foundations of Software Technology and Theoretical Computer Science, volume 182 of LIPIcs, pages 56:1-56:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. Google Scholar
  39. S. Schewe, Q. Tang, and T. Zhanabekova. Deciding what is good-for-MDPs. CoRR, abs/2202.07629, 2022. URL: https://arxiv.org/abs/2202.07629.
  40. S. Sickert, J. Esparza, S. Jaax, and J. Křetínský. Limit-deterministic Büchi automata for linear temporal logic. In Proc. 28th Int. Conf. on Computer Aided Verification, volume 9780 of Lecture Notes in Computer Science, pages 312-332. Springer, 2016. Google Scholar
  41. 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