Document Open Access Logo

Reducing (To) the Ranks: Efficient Rank-Based Büchi Automata Complementation

Authors Vojtěch Havlena , Ondřej Lengál

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2021.2.pdf
  • Filesize: 2.76 MB
  • 19 pages

Document Identifiers

Author Details

Vojtěch Havlena
  • Faculty of Information Technology, Brno University of Technology, Czech Republic
Ondřej Lengál
  • Faculty of Information Technology, Brno University of Technology, Czech Republic

Acknowledgements

We thank reviewers of this and previously submitted versions of the paper for their useful remarks that helped us improve the quality of the paper. This work was supported by the Czech Science Foundation project 20-07487S and the FIT BUT internal project FIT-S-20-6427.

Cite AsGet BibTex

Vojtěch Havlena and Ondřej Lengál. Reducing (To) the Ranks: Efficient Rank-Based Büchi Automata Complementation. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 2:1-2:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.CONCUR.2021.2

Abstract

This paper provides several optimizations of the rank-based approach for complementing Büchi automata. We start with Schewe’s theoretically optimal construction and develop a set of techniques for pruning its state space that are key to obtaining small complement automata in practice. In particular, the reductions (except one) have the property that they preserve (at least some) so-called super-tight runs, which are runs whose ranking is as tight as possible. Our evaluation on a large benchmark shows that the optimizations indeed significantly help the rank-based approach and that, in a large number of cases, the obtained complement is the smallest from those produced by state-of-the-art tools for Büchi complementation.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automata over infinite objects
Keywords
  • Büchi automata
  • rank-based complementation
  • super-tight runs

Metrics

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

Related Versions

References

  1. Joël D. Allred and Ulrich Ultes-Nitsche. A simple and optimal complementation algorithm for Büchi automata. In Proceedings of the Thirty third Annual IEEE Symposium on Logic in Computer Science (LICS 2018), pages 46-55. IEEE Computer Society Press, July 2018. Google Scholar
  2. 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 Daniel Kroening and Corina S. Pasareanu, editors, Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I, volume 9206 of Lecture Notes in Computer Science, pages 479-486. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-21690-4_31.
  3. Frantisek Blahoudek, Matthias Heizmann, Sven Schewe, Jan Strejcek, and Ming-Hsien Tsai. Complementing semi-deterministic Büchi automata. In Marsha Chechik and Jean-François Raskin, editors, Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, volume 9636 of Lecture Notes in Computer Science, pages 770-787. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-49674-9_49.
  4. František Blahoudek, Alexandre Duret-Lutz, and Jan Strejček. Seminator 2 can complement generalized Büchi automata via improved semi-determinization. In Proceedings of the 32nd International Conference on Computer-Aided Verification (CAV'20), volume 12225 of Lecture Notes in Computer Science, pages 15-27. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-53291-8_2.
  5. Bernard Boigelot, Sébastien Jodogne, and Pierre Wolper. On the use of weak automata for deciding linear arithmetic with integer and real variables. In Rajeev Goré, Alexander Leitsch, and Tobias Nipkow, editors, Automated Reasoning, First International Joint Conference, IJCAR 2001, Siena, Italy, June 18-23, 2001, Proceedings, volume 2083 of Lecture Notes in Computer Science, pages 611-625. Springer, 2001. URL: https://doi.org/10.1007/3-540-45744-5_50.
  6. Stefan Breuers, Christof Löding, and Jörg Olschewski. Improved Ramsey-based Büchi complementation. In Proc. of FOSSACS'12, pages 150-164. Springer, 2012. Google Scholar
  7. J. Richard Büchi. On a decision method in restricted second order arithmetic. In Proc. of International Congress on Logic, Method, and Philosophy of Science 1960. Stanford Univ. Press, Stanford, 1962. Google Scholar
  8. Yu-Fang Chen, Vojtech Havlena, and Ondrej Lengál. Simulations in rank-based Büchi automata complementation. In Anthony Widjaja Lin, editor, Programming Languages and Systems - 17th Asian Symposium, APLAS 2019, Nusa Dua, Bali, Indonesia, December 1-4, 2019, Proceedings, volume 11893 of Lecture Notes in Computer Science, pages 447-467. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-34175-6_23.
  9. Yu-Fang Chen, Matthias Heizmann, Ondrej Lengál, Yong Li, Ming-Hsien Tsai, Andrea Turrini, and Lijun Zhang. Advanced automata-based algorithms for program termination checking. In Jeffrey S. Foster and Dan Grossman, editors, Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, Philadelphia, PA, USA, June 18-22, 2018, pages 135-150. ACM, 2018. URL: https://doi.org/10.1145/3192366.3192405.
  10. Costas Courcoubetis and Mihalis Yannakakis. Verifying temporal properties of finite-state probabilistic programs. In 29th Annual Symposium on Foundations of Computer Science, White Plains, New York, USA, 24-26 October 1988, pages 338-345. IEEE Computer Society, 1988. URL: https://doi.org/10.1109/SFCS.1988.21950.
  11. Alexandre Duret-Lutz, Alexandre Lewkowicz, Amaury Fauchille, Thibaud Michaud, Étienne Renault, and Laurent Xu. Spot 2.0 - a framework for LTL and ω-automata manipulation. In Cyrille Artho, Axel Legay, and Doron Peled, editors, Automated Technology for Verification and Analysis, pages 122-129, Cham, 2016. Springer International Publishing. Google Scholar
  12. Seth Fogarty and Moshe Y. Vardi. Büchi complementation and size-change termination. In Proc. of TACAS'09, pages 16-30. Springer, 2009. Google Scholar
  13. Ehud Friedgut, Orna Kupferman, and Moshe Vardi. Büchi complementation made tighter. International Journal of Foundations of Computer Science, 17:851-868, 2006. Google Scholar
  14. Patrice Godefroid. Using partial orders to improve automatic verification methods. In Edmund M. Clarke and Robert P. Kurshan, editors, Computer Aided Verification, 2nd International Workshop, CAV '90, New Brunswick, NJ, USA, June 18-21, 1990, Proceedings, volume 531 of Lecture Notes in Computer Science, pages 176-185. Springer, 1990. URL: https://doi.org/10.1007/BFb0023731.
  15. Sankar Gurumurthy, Orna Kupferman, Fabio Somenzi, and Moshe Y. Vardi. On complementing nondeterministic Büchi automata. In Daniel Geist and Enrico Tronci, editors, Correct Hardware Design and Verification Methods, 12th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2003, L'Aquila, Italy, October 21-24, 2003, Proceedings, volume 2860 of Lecture Notes in Computer Science, pages 96-110. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-39724-3_10.
  16. Vojtěch Havlena and Ondřej Lengál. Reducing (to) the ranks: Efficient rank-based Büchi automata complementation (technical report). CoRR, abs/2010.07834, 2020. URL: http://arxiv.org/abs/2010.07834.
  17. Vojtěch Havlena and Ondřej Lengál. Ranker, 2021. URL: https://github.com/vhavlena/ba-inclusion.
  18. Matthias Heizmann, Jochen Hoenicke, and Andreas Podelski. Termination analysis by learning terminating programs. In Proc. of CAV'14, pages 797-813. Springer, 2014. Google Scholar
  19. Detlef Kähler and Thomas Wilke. Complementation, disambiguation, and determinization of Büchi automata unified. In Proc. of ICALP'08, pages 724-735. Springer, 2008. Google Scholar
  20. Hrishikesh Karmarkar and Supratik Chakraborty. On minimal odd rankings for Büchi complementation. In Zhiming Liu and Anders P. Ravn, editors, Automated Technology for Verification and Analysis, 7th International Symposium, ATVA 2009, Macao, China, October 14-16, 2009. Proceedings, volume 5799 of Lecture Notes in Computer Science, pages 228-243. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-04761-9_18.
  21. Joachim Klein and Christel Baier. On-the-fly stuttering in the construction of deterministic omega -automata. In Jan Holub and Jan Zdárek, editors, Implementation and Application of Automata, 12th International Conference, CIAA 2007, Prague, Czech Republic, July 16-18, 2007, Revised Selected Papers, volume 4783 of Lecture Notes in Computer Science, pages 51-61. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-76336-9_7.
  22. Orna Kupferman and Moshe Y. Vardi. Weak alternating automata are not that weak. ACM Trans. Comput. Log., 2(3):408-429, 2001. URL: https://doi.org/10.1145/377978.377993.
  23. Robert P. Kurshan. Complementing deterministic Büchi automata in polynomial time. J. Comput. Syst. Sci., 35(1):59-71, 1987. URL: https://doi.org/10.1016/0022-0000(87)90036-5.
  24. Yong Li, Xuechao Sun, Andrea Turrini, Yu-Fang Chen, and Junnan Xu. ROLL 1.0: ω-regular language learning library. In Tomás Vojnar and Lijun Zhang, editors, Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part I, volume 11427 of Lecture Notes in Computer Science, pages 365-371. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-17462-0_23.
  25. Yong Li, Andrea Turrini, Lijun Zhang, and Sven Schewe. Learning to complement Büchi automata. In Proc. of VMCAI'18, pages 313-335. Springer, 2018. Google Scholar
  26. Yong Li, Moshe Y. Vardi, and Lijun Zhang. On the power of unambiguity in Büchi complementation. In Jean-Francois Raskin and Davide Bresolin, editors, Proceedings 11th International Symposium on Games, Automata, Logics, and Formal Verification, Brussels, Belgium, September 21-22, 2020, volume 326 of Electronic Proceedings in Theoretical Computer Science, pages 182-198. Open Publishing Association, 2020. URL: https://doi.org/10.4204/EPTCS.326.12.
  27. Richard Mayr and Lorenzo Clemente. Advanced automata minimization. In Proc. of POPL'13, pages 63-74, 2013. Google Scholar
  28. Max Michel. Complementation is more difficult with automata on infinite words. CNET, Paris, 15, 1988. Google Scholar
  29. Doron A. Peled. All from one, one for all: on model checking using representatives. In Costas Courcoubetis, editor, Computer Aided Verification, 5th International Conference, CAV '93, Elounda, Greece, June 28 - July 1, 1993, Proceedings, volume 697 of Lecture Notes in Computer Science, pages 409-423. Springer, 1993. URL: https://doi.org/10.1007/3-540-56922-7_34.
  30. Nir Piterman. From nondeterministic Büchi and Streett automata to deterministic parity automata. In Proc. of LICS'06, pages 255-264. IEEE, 2006. Google Scholar
  31. Roman R. Redziejowski. An improved construction of deterministic omega-automaton using derivatives. Fundam. Informaticae, 119(3-4):393-406, 2012. URL: https://doi.org/10.3233/FI-2012-744.
  32. Shmuel Safra. On the complexity of ω-automata. In Proc. of FOCS'88, pages 319-327. IEEE, 1988. Google Scholar
  33. Sven Schewe. Büchi complementation made tight. In Susanne Albers and Jean-Yves Marion, editors, 26th International Symposium on Theoretical Aspects of Computer Science, STACS 2009, February 26-28, 2009, Freiburg, Germany, Proceedings, volume 3 of LIPIcs, pages 661-672. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany, 2009. URL: https://doi.org/10.4230/LIPIcs.STACS.2009.1854.
  34. Prasad A. Sistla, Moshe Y. Vardi, and Pierre Wolper. The complementation problem for Büchi automata with applications to temporal logic. In Automata, Languages and Programming, pages 465-474. Springer, 1985. Google Scholar
  35. Deian Tabakov and Moshe Y. Vardi. Experimental evaluation of classical automata constructions. In Proc. of LPAR'05, pages 396-411. Springer, 2005. Google Scholar
  36. Ming-Hsien Tsai, Seth Fogarty, Moshe Y. Vardi, and Yih-Kuen Tsay. State of Büchi complementation. In Michael Domaratzki and Kai Salomaa, editors, Implementation and Application of Automata, pages 261-271, Berlin, Heidelberg, 2011. Springer Berlin Heidelberg. Google Scholar
  37. Ming-Hsien Tsai, Yih-Kuen Tsay, and Yu-Shiang Hwang. GOAL for games, omega-automata, and logics. In Natasha Sharygina and Helmut Veith, editors, Computer Aided Verification, pages 883-889, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. Google Scholar
  38. Antti Valmari. Stubborn sets for reduced state space generation. In Grzegorz Rozenberg, editor, Advances in Petri Nets 1990, pages 491-515, Berlin, Heidelberg, 1991. Springer Berlin Heidelberg. Google Scholar
  39. Moshe Y. Vardi and Thomas Wilke. Automata: From logics to algorithms. Logic and Automata, 2:629-736, 2008. Google Scholar
  40. Qiqi Yan. Lower bounds for complementation of ω-automata via the full automata technique. In Michele Bugliesi, Bart Preneel, Vladimiro Sassone, and Ingo Wegener, editors, Automata, Languages and Programming, pages 589-600, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg. Google Scholar
  41. Qiqi Yan. Lower bounds for complementation of ω-automata via the full automata technique. In Proc. of ICALP'06, pages 589-600. Springer, 2006. 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