Document Open Access Logo

The Complexity of Simplifying ω-Automata Through the Alternating Cycle Decomposition

Authors Antonio Casares , Corto Mascle

PDF

File

Thumbnail PDF
PDF
LIPIcs.MFCS.2024.35.pdf
  • Filesize: 1.05 MB
  • 17 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Automata over infinite objects
Keywords
  • Omega-regular languages
  • Muller automata
  • Zielonka tree

Metrics

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

Abstract

In 2021, Casares, Colcombet and Fijalkow introduced the Alternating Cycle Decomposition (ACD), a structure used to define optimal transformations of Muller into parity automata and to obtain theoretical results about the possibility of relabelling automata with different acceptance conditions. In this work, we study the complexity of computing the ACD and its DAG-version, proving that this can be done in polynomial time for suitable representations of the acceptance condition of the Muller automaton. As corollaries, we obtain that we can decide typeness of Muller automata in polynomial time, as well as the parity index of the languages they recognise.
Furthermore, we show that we can minimise in polynomial time the number of colours (resp. Rabin pairs) defining a Muller (resp. Rabin) acceptance condition, but that these problems become NP-complete when taking into account the structure of an automaton using such a condition.

Cite As Get BibTex

Antonio Casares and Corto Mascle. The Complexity of Simplifying ω-Automata Through the Alternating Cycle Decomposition. In 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 306, pp. 35:1-35:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.MFCS.2024.35

Author Details

Antonio Casares
  • University of Warsaw, Poland
Corto Mascle
  • LaBRI, Université de Bordeaux, France

Funding

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

References

  1. Tomáš Babiak, František Blahoudek, Alexandre Duret-Lutz, Joachim Klein, Jan Křetínský, David Müller, David Parker, and Jan Strejček. The Hanoi omega-automata format. In CAV, pages 479-486, 2015. URL: https://doi.org/10.1007/978-3-319-21690-4_31.
  2. Christel Baier, František Blahoudek, Alexandre Duret-Lutz, Joachim Klein, David Müller, and Jan Strejček. Generic emptiness check for fun and profit. In ATVA, pages 445-461, 2019. URL: https://doi.org/10.1007/978-3-030-31784-3_26.
  3. Udi Boker. Why these automata types? In LPAR, volume 57 of EPiC Series in Computing, pages 143-163, 2018. URL: https://doi.org/10.29007/c3bj.
  4. Endre Boros and Ondřej Čepek. On the complexity of Horn minimization. Rutgers University. Rutgers Center for Operations Research [RUTCOR], 1994. Google Scholar
  5. 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
  6. Cristian S. Calude, Sanjay Jain, Bakhadyr Khoussainov, Wei Li, and Frank Stephan. Deciding parity games in quasi-polynomial time. SIAM Journal on Computing, 51(2):STOC17-152-STOC17-188, 2022. URL: https://doi.org/10.1137/17M1145288.
  7. Olivier Carton and Ramón Maceiras. Computing the Rabin index of a parity automaton. RAIRO, pages 495-506, 1999. URL: https://doi.org/10.1051/ita:1999129.
  8. 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.
  9. Antonio Casares, Thomas Colcombet, and Nathanaël Fijalkow. Optimal transformations of games and automata using Muller conditions. In ICALP, volume 198, pages 123:1-123:14, 2021. URL: https://doi.org/10.4230/LIPIcs.ICALP.2021.123.
  10. 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.
  11. 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.
  12. Antonio Casares, Alexandre Duret-Lutz, Klara J. Meyer, Florian Renkin, and Salomon Sickert. Practical applications of the Alternating Cycle Decomposition. In TACAS, volume 13244 of Lecture Notes in Computer Science, pages 99-117, 2022. URL: https://doi.org/10.1007/978-3-030-99527-0_6.
  13. Antonio Casares and Corto Mascle. The complexity of simplifying ω-automata through the alternating cycle decomposition. CoRR, abs/2401.03811, 2024. URL: https://doi.org/10.48550/arXiv.2401.03811.
  14. Tom Chang. Horn formula minimization. Master’s thesis, Rochester Institute of Technology, 2006. Available at URL: https://scholarworks.rit.edu/cgi/viewcontent.cgi?article=7895&context=theses.
  15. William F Dowling and Jean H Gallier. Linear-time algorithms for testing the satisfiability of propositional Horn formulae. The Journal of Logic Programming, 1(3):267-284, 1984. Google Scholar
  16. Alexandre Duret-Lutz, Etienne Renault, Maximilien Colange, Florian Renkin, Alexandre Gbaguidi Aisse, Philipp Schlehuber-Caissier, Thomas Medioni, Antoine Martin, Jérôme Dubois, Clément Gillard, and Henrich Lauko. From Spot 2.0 to Spot 2.10: What’s new? In CAV, volume 13372 of Lecture Notes in Computer Science, pages 174-187, 2022. URL: https://doi.org/10.1007/978-3-031-13188-2_9.
  17. Stefan Dziembowski, Marcin Jurdziński, and Igor Walukiewicz. How much memory is needed to win infinite games? In LICS, pages 99-110, 1997. URL: https://doi.org/10.1109/LICS.1997.614939.
  18. E. Allen Emerson, Charanjit S. Jutla, and A. Prasad Sistla. On model-checking for fragments of μ-calculus. In CAV, volume 697 of Lecture Notes in Computer Science, pages 385-396, 1993. URL: https://doi.org/10.1007/3-540-56922-7_32.
  19. Javier Esparza, Jan Křetínský, Jean-François Raskin, and Salomon Sickert. From LTL and limit-deterministic Büchi automata to deterministic parity automata. In TACAS, pages 426-442, 2017. URL: https://doi.org/10.1007/978-3-662-54577-5_25.
  20. Peter L Hammer and Alexander Kogan. Optimal compression of propositional Horn knowledge bases: complexity and approximation. Artificial Intelligence, 64(1):131-145, 1993. Google Scholar
  21. Christopher Hugenroth. Zielonka DAG acceptance and regular languages over infinite words. In DLT, volume 13911 of Lecture Notes in Computer Science, pages 143-155, 2023. URL: https://doi.org/10.1007/978-3-031-33264-7_12.
  22. Paul Hunter and Anuj Dawar. Complexity bounds for regular games. In MFCS, pages 495-506, 2005. URL: https://doi.org/10.1007/11549345_43.
  23. Paul Hunter and Anuj Dawar. Complexity bounds for Muller games. Theoretical Computer Science (TCS), 2008. Google Scholar
  24. Swen Jacobs, Guillermo A. Perez, Remco Abraham, Veronique Bruyere, Michael Cadilhac, Maximilien Colange, Charly Delfosse, Tom van Dijk, Alexandre Duret-Lutz, Peter Faymonville, Bernd Finkbeiner, Ayrat Khalimov, Felix Klein, Michael Luttenberger, Klara Meyer, Thibaud Michaud, Adrien Pommellet, Florian Renkin, Philipp Schlehuber-Caissier, Mouhammad Sakr, Salomon Sickert, Gaetan Staquet, Clement Tamines, Leander Tentrup, and Adam Walker. The reactive synthesis competition (SYNTCOMP): 2018-2021, 2022. URL: https://arxiv.org/abs/2206.00251.
  25. Sriram C. Krishnan, Anuj Puri, and Robert K. Brayton. Structural complexity of omega-automata. In STACS, pages 143-156, 1995. URL: https://doi.org/10.1007/3-540-59042-0_69.
  26. Orna Kupferman, Gila Morgenstern, and Aniello Murano. Typeness for omega-regular automata. Int. J. Found. Comput. Sci., 17(4):869-884, 2006. URL: https://doi.org/10.1142/S0129054106004157.
  27. Jan Křetínský, Tobias Meggendorfer, and Salomon Sickert. Owl: A library for ω-words, automata, and LTL. In ATVA, volume 11138 of Lecture Notes in Computer Science, pages 543-550, 2018. URL: https://doi.org/10.1007/978-3-030-01090-4_34.
  28. Christof Löding. Optimal bounds for transformations of ω-automata. In FSTTCS, pages 97-109, 1999. URL: https://doi.org/10.1007/3-540-46691-6_8.
  29. Michael Luttenberger, Philipp J. Meyer, and Salomon Sickert. Practical synthesis of reactive systems from LTL specifications via parity games. Acta Informatica, pages 3-36, 2020. URL: https://doi.org/10.1007/s00236-019-00349-3.
  30. Robert McNaughton. Testing and generating infinite sequences by a finite automaton. Information and control, 9(5):521-530, 1966. URL: https://doi.org/10.1016/S0019-9958(66)80013-X.
  31. Philipp Meyer and Salomon Sickert. On the optimal and practical conversion of Emerson-Lei automata into parity automata. Unpublished manuscript, obsoleted by the work of [Casares et al., 2021], 2021. Google Scholar
  32. Philipp J. Meyer and Salomon Sickert. Modernising Strix. SYNT Workshop, 2021. URL: https://www7.in.tum.de/~sickert/publications/MeyerS21.pdf.
  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. Andrzej W. Mostowski. Regular expressions for infinite trees and a standard form of automata. In SCT, pages 157-168, 1984. URL: https://doi.org/10.1007/3-540-16066-3_15.
  35. David Müller and Salomon Sickert. LTL to deterministic Emerson-Lei automata. In GandALF, pages 180-194, 2017. URL: https://doi.org/10.4204/EPTCS.256.13.
  36. Nir Piterman and Amir Pnueli. Faster solutions of Rabin and Streett games. In LICS,, pages 275-284. IEEE Computer Society, 2006. URL: https://doi.org/10.1109/LICS.2006.23.
  37. 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.
  38. Michael O. Rabin. Decidability of second-order theories and automata on infinite trees. Transactions of the American Mathematical Society, 141:1-35, 1969. URL: http://www.jstor.org/stable/1995086.
  39. Tereza Schwarzová, Jan Strejček, and Juraj Major. Reducing acceptance marks in Emerson-Lei automata by QBF solving. In SAT, volume 271, pages 23:1-23:20, 2023. URL: https://doi.org/10.4230/LIPIcs.SAT.2023.23.
  40. Cong Tian and Zhenhua Duan. Büchi determinization made tighter. CoRR, abs/1404.1436, 2014. URL: https://arxiv.org/abs/1404.1436.
  41. Thomas Wilke and Haiseung Yoo. Computing the Rabin index of a regular language of infinite words. Inf. Comput., pages 61-70, 1996. URL: https://doi.org/10.1006/inco.1996.0082.
  42. Wiesław Zielonka. Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theoretical Computer Science, 200(1-2):135-183, 1998. URL: https://doi.org/10.1016/S0304-3975(98)00009-7.
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