Document Open Access Logo

Between Deterministic and Nondeterministic Quantitative Automata (Invited Talk)

Author Udi Boker

PDF
Thumbnail PDF

File

LIPIcs.CSL.2022.1.pdf
  • Filesize: 0.69 MB
  • 15 pages

Document Identifiers

Author Details

Udi Boker
  • Reichman University, Herzliya, Israel

Acknowledgements

We thank Karoliina Lehtinen for stimulating discussions on prelimiary versions of the paper, and specifically for suggesting the all-thresholds generalization of the notions.

Cite AsGet BibTex

Udi Boker. Between Deterministic and Nondeterministic Quantitative Automata (Invited Talk). In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 1:1-1:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.CSL.2022.1

Abstract

There is a challenging trade-off between deterministic and nondeterministic automata, where the former suit various applications better, however at the cost of being exponentially larger or even less expressive. This gave birth to many notions in between determinism and nondeterminism, aiming at enjoying, sometimes, the best of both worlds. Some of the notions are yes/no ones, for example initial nondeterminism (restricting nondeterminism to allowing several initial states), and some provide a measure of nondeterminism, for example the ambiguity level. We analyze the possible generalization of such notions from Boolean to quantitative automata, and suggest that it depends on the following key characteristics of the considered notion 𝖭 - whether it is syntactic or semantic, and if semantic, whether it is word-based or language-based. A syntactic notion, such as initial nondeterminism, applies as is to a quantitative automaton A, namely 𝖭(A). A word-based semantic notion, such as unambiguity, applies as is to a Boolean automaton t-A that is derived from A by accompanying it with some threshold value t ∈ ℝ, namely 𝖭(t-A). A language-based notion, such as history determinism, also applies as is to t-A, while in addition, it naturally generalizes into two different notions with respect to A itself, by either: i) taking the supremum of 𝖭(t-A) over all thresholds t, denoted by Threshold-𝖭(A); or ii) generalizing the basis of the notion from a language to a function, denoted simply by 𝖭(A). While in general 𝖭(A) ⇒ Threshold-𝖭(A) ⇒ 𝖭(t-A), we have for some notions 𝖭(A) ≡ Threshold-𝖭(A), and for some not. (For measure notions, ⇒ stands for ≥ with respect to the nondeterminism level.) We classify numerous notions known in the Boolean setting according to their characterization above, generalize them to the quantitative setting and look into relations between them. The generalized notions open new research directions with respect to quantitative automata, and provide insights on the original notions with respect to Boolean automata.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Quantitative Automata
  • Measure of Nondeterminism
  • Determinism

Metrics

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

References

  1. Bader Abu Radi, Orna Kupferman, and Ofer Leshkowitz. A hierarchy of nondeterminism. In Proc. of MFCS, volume 202 of LIPIcs, pages 85:1-85:21, 2021. Google Scholar
  2. Shaull Almagor, Udi Boker, and Orna Kupferman. Formalizing and reasoning about quality. Journal of the ACM, 63(3):24:1-24:56, 2016. Google Scholar
  3. Shaull Almagor, Orna Kupferman, Jan Oliver Ringert, and Yaron Velner. Quantitative assume guarantee synthesis. In Proc. of CAV, pages 353-374. Springer, 2017. Google Scholar
  4. Benjamin Aminof, Orna Kupferman, and Robby Lampert. Reasoning about online algorithms with weighted automata. ACM Transactions on Algorithms, 6(2):28:1-28:36, 2010. Google Scholar
  5. Marc Bagnol and Denis Kuperberg. Büchi good-for-games automata are efficiently recognizable. In Proc. of FSTTCS, page 16, 2018. Google Scholar
  6. Roderick Bloem, Krishnendu Chatterjee, Thomas A. Henzinger, and Barbara Jobstmann. Better quality in synthesis through quantitative objectives. In Proc. of CAV, pages 140-156, 2009. Google Scholar
  7. Udi Boker. Why these automata types? In Proc. of LPAR, pages 143-163, 2018. Google Scholar
  8. Udi Boker. Quantitative vs. weighted automata. In Proc. of RP, pages 1-16, 2021. Google Scholar
  9. Udi Boker, Krishnendu Chatterjee, Thomas A. Henzinger, and Orna Kupferman. Temporal specifications with accumulative values. ACM Trans. Comput. Log., 15(4):27:1-27:25, 2014. Google Scholar
  10. Udi Boker, Denis Kuperberg, Orna Kupferman, and Michał Skrzypczak. Nondeterminism in the presence of a diverse or unknown future. In Proc. of ICALP, pages 89-100, 2013. Google Scholar
  11. Udi Boker, Denis Kuperberg, Karoliina Lehtinen, and Michał Skrzypczak. On succinctness and recognisability of alternating good-for-games automata. arXiv:2002.07278, 2020. Google Scholar
  12. Udi Boker and Karoliina Lehtinen. Token games and history deterministic quantitative automata. Submitted. Google Scholar
  13. Udi Boker and Karoliina Lehtinen. Good for games automata: From nondeterminism to alternation. In Proc. of CONCUR, pages 19:1-19:16, 2019. Google Scholar
  14. Udi Boker and Karoliina Lehtinen. History determinism vs. good for gameness in quantitative automata. In Proc. of FSTTCS, pages 35:1-35:20, 2021. Google Scholar
  15. Romain Brenguier, Lorenzo Clemente, Paul Hunter, Guillermo A Pérez, Mickael Randour, Jean-François Raskin, Ocan Sankur, and Mathieu Sassolas. Non-zero sum games for reactive synthesis. In Proc. of LATA, pages 3-23, 2016. Google Scholar
  16. Krishnendu Chatterjee, Laurent Doyen, and Thomas A. Henzinger. Alternating weighted automata. In Proceedings of FCT, pages 3-13, 2009. Google Scholar
  17. Krishnendu Chatterjee, Laurent Doyen, and Thomas A. Henzinger. Quantitative languages. ACM Trans. Comput. Log., 11(4):23:1-23:38, 2010. Google Scholar
  18. Krishnendu Chatterjee, Thomas A Henzinger, Barbara Jobstmann, and Rohit Singh. Quasy: Quantitative synthesis tool. In Proc. of TACAS, pages 267-271. Springer, 2011. Google Scholar
  19. Thomas Colcombet. The theory of stabilisation monoids and regular cost functions. In Proc. of ICALP, pages 139-150, 2009. Google Scholar
  20. Thomas Colcombet. Fonctions régulières de coût. Habilitation à diriger les recherches, École Doctorale de Sciences Mathématiques de Paris Centre, 2013. Google Scholar
  21. Thomas Colcombet. Unambiguity in automata theory. In Proc. of DCFS, pages 3-18, 2015. Google Scholar
  22. Thomas Colcombet and Nathanaël Fijalkow. Universal graphs and good for games automata: New tools for infinite duration games. In Proc. of FOSSACS, pages 1-26, 2019. Google Scholar
  23. Costas Courcoubetis and Mihalis Yannakakis. The complexity of probabilistic verification. J. ACM, 42(4):857-907, 1995. Google Scholar
  24. Laurent Doyen. Games and automata: From Boolean to quantitative verification. Habilitation Thesis, École Normale Supérieure de Cachan, 2011. Google Scholar
  25. Marco Faella, Axel Legay, and Mariëlle Stoelinga. Model checking quantitative linear time logic. Electr. Notes Theor. Comput. Sci., 220(3):61-77, 2008. Google Scholar
  26. Emmanuel Filiot, Ismaël Jecker, Nathan Lhote, Guillermo A. Pérez, and Jean-François Raskin. On delay and regret determinization of max-plus automata. In LICS, pages 1-12, 2017. Google Scholar
  27. Emmanuel Filiot, Christof Löding, and Sarah Winter. Synthesis from weighted specifications with partial domains over finite words. In FSTTCS, pages 46:1-46:16, 2020. Google Scholar
  28. Daniel Goč and Kai Salomaa. Computation width and deviation number. In Descriptional Complexity of Formal Systems, pages 150-161, 2014. Google Scholar
  29. Jonathan Goldstine, Chandra M. R. Kintala, and Detlef Wotschke. On measuring nondeterminism in regular languages. Inf. Comput., 86(2):179-194, 1990. Google Scholar
  30. Mika Göös and Stefan Kiefer. Lower bounds on unambiguous automata complementation and separation via communication complexity. CoRR, abs/2109.09155, 2021. URL: http://arxiv.org/abs/2109.09155.
  31. Ernst Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, and Dominik Wojtczak. Good-for-MDPs automata for probabilistic analysis and reinforcement learning. In Proc. of TACAS, pages 306-323, 2020. Google Scholar
  32. Thomas Henzinger and Nir Piterman. Solving games without determinization. In Proc. of CSL, pages 395-410, 2006. Google Scholar
  33. Markus Holzer, Kai Salomaa, and Sheng Yu. On the state complexity of k-entry deterministic finite automata. J. Autom. Lang. Comb., 6(4):453-466, 2001. Google Scholar
  34. Juraj Hromkovič, Juhani Karhumäki, Hartmut Klauck, Georg Schnitger, and Sebastian Seibert. Measures of nondeterminism in finite automata. In Proc. of ICALP, pages 199-210, 2000. Google Scholar
  35. Juraj Hromkovic, Sebastian Seibert, Juhani Karhumäki, Hartmut Klauck, and Georg Schnitger. Communication complexity method for measuring nondeterminism in finite automata. Inf. Comput., 172(2):202-217, 2002. Google Scholar
  36. Paul Hunter, Guillermo A. Pérez, and Jean-François Raskin. Reactive synthesis without regret. Acta Informatica, 54(1):3-39, 2017. Google Scholar
  37. Martin Kappes. Descriptional complexity of deterministic finite automata with multiple initial states. Journal of Automata, Languages and Combinatorics, 5:269-278, January 2000. Google Scholar
  38. Chris Keeler and Kai Salomaa. Branching measures and nearly acyclic NFAs. Int. J. Found. Comput. Sci., 30(6-7):1135-1155, 2019. Google Scholar
  39. Chris Keeler and Kai Salomaa. Alternating finite automata with limited universal branching. In Proc. of LATA, pages 196-207, 2020. Google Scholar
  40. Chandra M. R. Kintala. Refining nondeterminism in context-free languages. Math. Syst. Theory, 12:1-8, 1978. Google Scholar
  41. Chandra M. R. Kintala and Patrick C. Fischer. Computations with a restricted number of nondeterministic steps (extended abstract). In Proc. of STOC, pages 178-185, 1977. Google Scholar
  42. Chandra M. R. Kintala and Detlef Wotschke. Amounts of nondeterminism in finite automata. Acta Informatica, 13:199-204, 1980. Google Scholar
  43. Denis Kuperberg and Michał Skrzypczak. On determinisation of good-for-games automata. In Proc. of ICALP, pages 299-310, 2015. Google Scholar
  44. Karoliina Lehtinen and Udi Boker. Register games. Log. Methods Comput. Sci., 16(2), 2020. Google Scholar
  45. Hing Leung. Structurally unambiguous finite automata. In Proc. of CIAA, pages 198-207, 2006. Google Scholar
  46. Christof Löding and Stefan Repke. Decidability results on the existence of lookahead delegators for NFA. In Proc. of FSTTCS, pages 327-338, 2013. Google Scholar
  47. Christof Löding and Andreas Tollkötter. State space reduction for parity automata. In Proc. of CSL, pages 27:1-27:16, 2020. Google Scholar
  48. Anirban Majumdar and Denis Kuperberg. Computing the width of non-deterministic automata. Logical Methods in Computer Science, 15, 2019. Google Scholar
  49. Alexandros Palioudakis, Kai Salomaa, and Selim Akl. Comparisons between measures of nondeterminism on finite automata. In Proc. of DCFS, pages 217-228, 2013. Google Scholar
  50. Mikhail A. Raskin. A superpolynomial lower bound for the size of non-deterministic complement of an unambiguous automaton. In Proc. of ICALP, pages 138:1-138:11, 2018. Google Scholar
  51. Bala Ravikumar and Nicolae Santean. On the existence of lookahead delegators for NFA. Int. J. Found. Comput. Sci., 18(5):949-973, 2007. Google Scholar
  52. M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification (preliminary report). In Proc. of LICS, pages 332-344, 1986. 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