Document Open Access Logo

On the Minimisation of Deterministic and History-Deterministic Generalised (Co)Büchi Automata

Authors Antonio Casares , Olivier Idir, Denis Kuperberg , Corto Mascle , Aditya Prakash

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2025.22.pdf
  • Filesize: 1.06 MB
  • 18 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Verification by model checking
Keywords
  • Automata minimisation
  • omega-regular languages
  • good-for-games automata

Metrics

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

Abstract

We present a polynomial-time algorithm minimising the number of states of history-deterministic generalised coBüchi automata, building on the work of Abu Radi and Kupferman on coBüchi automata. On the other hand, we establish that the minimisation problem for both deterministic and history-deterministic generalised Büchi automata is NP-complete, as well as the problem of minimising at the same time the number of states and colours of history-deterministic generalised coBüchi automata.

Cite As Get BibTex

Antonio Casares, Olivier Idir, Denis Kuperberg, Corto Mascle, and Aditya Prakash. On the Minimisation of Deterministic and History-Deterministic Generalised (Co)Büchi Automata. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 22:1-22:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CSL.2025.22

Author Details

Antonio Casares
  • University of Warsaw, Poland
Olivier Idir
  • IRIF, Université Paris-Cité, France
Denis Kuperberg
  • LIP, CNRS, ENS Lyon, France
Corto Mascle
  • LaBRI, Université de Bordeaux, France
  • Max Planck Institute for Software Systems (MPI-SWS), Kaiserslautern, Germany
Aditya Prakash
  • University of Warwick, UK

Funding

  • Casares, Antonio: Supported by the Polish National Science Centre (NCN) grant “Polynomial finite state computation” (2022/46/A/ST6/00072).

References

  1. Bader Abu Radi and Orna Kupferman. Minimizing GFG transition-based automata. In ICALP, volume 132 of LIPIcs, pages 100:1-100:16, 2019. URL: https://doi.org/10.4230/LIPIcs.ICALP.2019.100.
  2. Bader Abu Radi and Orna Kupferman. Minimization and canonization of GFG transition-based automata. Log. Methods Comput. Sci., 18(3), 2022. URL: https://doi.org/10.46298/lmcs-18(3:16)2022.
  3. Souheib Baarir and Alexandre Duret-Lutz. Mechanizing the minimization of deterministic generalized Büchi automata. In FORTE, volume 8461 of Lecture Notes in Computer Science, pages 266-283, 2014. URL: https://doi.org/10.1007/978-3-662-43613-4_17.
  4. Marc Bagnol and Denis Kuperberg. Büchi good-for-games automata are efficiently recognizable. In FSTTCS, page 16, 2018. URL: https://doi.org/10.4230/LIPICS.FSTTCS.2018.16.
  5. Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008. Google Scholar
  6. Frantisek Blahoudek, Alexandre Duret-Lutz, and Jan Strejcek. Seminator 2 can complement generalized Büchi automata via improved semi-determinization. In CAV, volume 12225 of Lecture Notes in Computer Science, pages 15-27, 2020. URL: https://doi.org/10.1007/978-3-030-53291-8_2.
  7. Udi Boker, Denis Kuperberg, Orna Kupferman, and Michal Skrzypczak. Nondeterminism in the presence of a diverse or unknown future. In Automata, Languages, and Programming - 40th International Colloquium, ICALP 2013, volume 7966 of Lecture Notes in Computer Science, pages 89-100. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39212-2_11.
  8. Udi Boker, Denis Kuperberg, Karoliina Lehtinen, and Michał Skrzypczak. On succinctness and recognisability of alternating good-for-games automata. CoRR, abs/2002.07278, 2020. URL: https://arxiv.org/abs/2002.07278.
  9. Udi Boker and Karoliina Lehtinen. Good for games automata: From nondeterminism to alternation. In CONCUR, volume 140, pages 19:1-19:16, 2019. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2019.19.
  10. Udi Boker and Karoliina Lehtinen. History determinism vs. good for gameness in quantitative automata. In FSTTCS, volume 213, pages 38:1-38:20, 2021. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2021.38.
  11. Udi Boker and Karoliina Lehtinen. When a little nondeterminism goes a long way: An introduction to history-determinism. ACM SIGLOG News, 10(1):24-51, 2023. URL: https://doi.org/10.1145/3584676.3584682.
  12. Patricia Bouyer, Antonio Casares, Mickael Randour, and Pierre Vandenhove. Half-positional objectives recognized by deterministic Büchi automata. In CONCUR, volume 243, pages 20:1-20:18, 2022. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2022.20.
  13. J. Richard Büchi and Lawrence H. Landweber. Solving sequential conditions by finite-state strategies. Transactions of the American Mathematical Society, 138:295-311, 1969. URL: http://www.jstor.org/stable/1994916.
  14. J. Richard Büchi. On a decision method in restricted second order arithmetic. Proc. Internat. Congr. on Logic, Methodology and Philosophy of Science, pages 1-11, 1962. Google Scholar
  15. Antonio Casares. On the minimisation of transition-based Rabin automata and the chromatic memory requirements of Muller conditions. In CSL, volume 216, pages 12:1-12:17, 2022. URL: https://doi.org/10.4230/LIPIcs.CSL.2022.12.
  16. Antonio Casares. Structural properties of automata over infinite words and memory for games (Propriétés structurelles des automates sur les mots infinis et mémoire pour les jeux). PhD thesis, Université de Bordeaux, France, 2023. URL: https://theses.hal.science/tel-04314678.
  17. Antonio Casares, Thomas Colcombet, Nathanaël Fijalkow, and Karoliina Lehtinen. From Muller to Parity and Rabin Automata: Optimal Transformations Preserving (History) Determinism. TheoretiCS, Volume 3, April 2024. URL: https://doi.org/10.46298/theoretics.24.12.
  18. Antonio Casares, Thomas Colcombet, and Karoliina Lehtinen. On the size of good-for-games Rabin automata and its link with the memory in Muller games. In ICALP, volume 229, pages 117:1-117:20, 2022. URL: https://doi.org/10.4230/LIPIcs.ICALP.2022.117.
  19. Antonio Casares and Corto Mascle. The complexity of simplifying ω-automata through the alternating cycle decomposition. CoRR, abs/2401.03811, 2024. https://arxiv.org/abs/2401.03811, URL: https://doi.org/10.48550/arXiv.2401.03811.
  20. Thomas Colcombet. The theory of stabilisation monoids and regular cost functions. In ICALP, pages 139-150, 2009. URL: https://doi.org/10.1007/978-3-642-02930-1_12.
  21. Costas Courcoubetis, Moshe Y. Vardi, Pierre Wolper, and Mihalis Yannakakis. Memory-efficient algorithms for the verification of temporal properties. Formal Methods Syst. Des., 1(2/3):275-288, 1992. URL: https://doi.org/10.1007/BF00121128.
  22. Alexandre Duret-Lutz, Alexandre Lewkowicz, Amaury Fauchille, Thibaud Michaud, Etienne Renault, and Laurent Xu. Spot 2.0 - A framework for LTL and ω-automata manipulation. In ATVA, volume 9938 of Lecture Notes in Computer Science, pages 122-129, 2016. URL: https://doi.org/10.1007/978-3-319-46520-3_8.
  23. Rüdiger Ehlers. Minimising deterministic Büchi automata precisely using SAT solving. In Theory and Applications of Satisfiability Testing - SAT, volume 6175 of Lecture Notes in Computer Science, pages 326-332, 2010. URL: https://doi.org/10.1007/978-3-642-14186-7_28.
  24. Javier Esparza, Orna Kupferman, and Moshe Y. Vardi. Verification. In Jean-Éric Pin, editor, Handbook of Automata Theory, pages 1415-1456. European Mathematical Society Publishing House, Zürich, Switzerland, 2021. URL: https://doi.org/10.4171/AUTOMATA-2/16.
  25. Rob Gerth, Doron A. Peled, Moshe Y. Vardi, and Pierre Wolper. Simple on-the-fly automatic verification of linear temporal logic. In IFIP, volume 38, pages 3-18, 1995. Google Scholar
  26. Thomas A. Henzinger and Nir Piterman. Solving games without determinization. In Computer Science Logic, pages 395-410, 2006. URL: https://doi.org/10.1007/11874683_26.
  27. John E. Hopcroft. An n log n algorithm for minimizing states in a finite automaton. Technical report, Stanford University, 1971. URL: https://doi.org/10.5555/891883.
  28. Christopher Hugenroth. Zielonka DAG acceptance, regular languages over infinite words. In DLT, 2023. Google Scholar
  29. Sudeep Juvekar and Nir Piterman. Minimizing generalized Büchi automata. In CAV, pages 45-58, 2006. URL: https://doi.org/10.1007/11817963_7.
  30. Denis Kuperberg and Michał Skrzypczak. On determinisation of good-for-games automata. In ICALP, pages 299-310, 2015. URL: https://doi.org/10.1007/978-3-662-47666-6_24.
  31. Orna Kupferman, Shmuel Safra, and Moshe Y. Vardi. Relating word and tree automata. In LICS, pages 322-332, 1996. URL: https://doi.org/10.1109/LICS.1996.561360.
  32. Karoliina Lehtinen and Martin Zimmermann. Good-for-games ω-pushdown automata. In LICS, pages 689-702, 2020. URL: https://doi.org/10.1145/3373718.3394737.
  33. Thibaud Michaud and Maximilien Colange. Reactive synthesis from LTL specification with Spot. In SYNT@CAV, Electronic Proceedings in Theoretical Computer Science, 2018. Google Scholar
  34. Satoru Miyano and Takeshi Hayashi. Alternating finite automata on omega-words. Theor. Comput. Sci., 32:321-330, 1984. URL: https://doi.org/10.1016/0304-3975(84)90049-5.
  35. Amir Pnueli and Roni Rosner. On the synthesis of a reactive module. In POPL, pages 179-190, 1989. URL: https://doi.org/10.1145/75277.75293.
  36. Etienne Renault, Alexandre Duret-Lutz, Fabrice Kordon, and Denis Poitrenaud. Three SCC-based emptiness checks for generalized Büchi automata. In LPAR, volume 8312 of Lecture Notes in Computer Science, pages 668-682, 2013. URL: https://doi.org/10.1007/978-3-642-45221-5_44.
  37. Etienne Renault, Alexandre Duret-Lutz, Fabrice Kordon, and Denis Poitrenaud. Variations on parallel explicit emptiness checks for generalized Büchi automata. Int. J. Softw. Tools Technol. Transf., 19(6):653-673, 2017. URL: https://doi.org/10.1007/S10009-016-0422-5.
  38. Schmuel Safra. On the complexity of ω-automata. In FOCS, pages 319-327, 1988. URL: https://doi.org/10.1109/SFCS.1988.21948.
  39. Sven Schewe. Beyond hyper-minimisation - minimising DBAs and DPAs is NP-complete. In FSTTCS, volume 8, pages 400-411, 2010. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2010.400.
  40. Sven Schewe. Minimising Good-For-Games automata is NP-complete. In FSTTCS, volume 182, pages 56:1-56:13, 2020. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2020.56.
  41. Fabio Somenzi and Roderick Bloem. Efficient Büchi automata from LTL formulae. In CAV, volume 1855 of Lecture Notes in Computer Science, pages 248-263, 2000. URL: https://doi.org/10.1007/10722167_21.
  42. M.Y. Vardi and P. Wolper. Reasoning about infinite computations. Information and Computation, 115(1):1-37, 1994. URL: https://doi.org/10.1006/inco.1994.1092.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact