Document Open Access Logo

Inclusion Testing of Büchi Automata Based on Well-Quasiorders

Authors Kyveli Doveri , Pierre Ganty , Francesco Parolini , Francesco Ranzato

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2021.3.pdf
  • Filesize: 1.01 MB
  • 22 pages

Document Identifiers

Author Details

Kyveli Doveri
  • IMDEA Software Institute, Madrid, Spain
  • Universidad Politécnica de Madrid, Spain
Pierre Ganty
  • IMDEA Software Institute, Madrid, Spain
Francesco Parolini
  • Sorbonne Université, Paris, France
Francesco Ranzato
  • University of Padova, Italy

Funding

  • Ganty, Pierre: Partially supported by the Madrid regional project S2018/TCS-4339 BLOQUES, the Spanish project PGC2018-102210-B-I00 BOSCO and the Ramón y Cajal fellowship RYC-2016-20281.
  • Ranzato, Francesco: Partially funded by University of Padova, under the SID2018 project "Analysis of STatic Analyses (ASTA)"; Italian Ministry of University and Research, under the PRIN2017 project no. 201784YSZ5 "AnalysiS of PRogram Analyses (ASPRA)"; Facebook Research, under a "Probability and Programming Research Award".

Acknowledgements

We thank: Richard Mayr, Lorenzo Clemente, Parosh Abdulla and Lukáš Holík for their insights and help with RABIT; Ming-Hsien Tsai for his help with GOAL; Reed Oei for the Pecan benchmarks; Matthias Heizmann and Daniel Dietsch for the Ultimate Automizer benchmarks.

Cite AsGet BibTex

Kyveli Doveri, Pierre Ganty, Francesco Parolini, and Francesco Ranzato. Inclusion Testing of Büchi Automata Based on Well-Quasiorders. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 3:1-3:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.CONCUR.2021.3

Abstract

We introduce an algorithmic framework to decide whether inclusion holds between languages of infinite words over a finite alphabet. Our approach falls within the class of Ramsey-based methods and relies on a least fixpoint characterization of ω-languages leveraging ultimately periodic infinite words of type uv^ω, with u a finite prefix and v a finite period of an infinite word. We put forward an inclusion checking algorithm between Büchi automata, called BAInc, designed as a complete abstract interpretation using a pair of well-quasiorders on finite words. BAInc is quite simple: it consists of two least fixpoint computations (one for prefixes and the other for periods) manipulating finite sets (of pairs) of states compared by set inclusion, so that language inclusion holds when the sets (of pairs) of states of the fixpoints satisfy some basic conditions. We implemented BAInc in a tool called BAIT that we experimentally evaluated against the state-of-the-art. We gathered, in addition to existing benchmarks, a large number of new case studies stemming from program verification and word combinatorics, thereby significantly expanding both the scope and size of the available benchmark set. Our experimental results show that BAIT advances the state-of-the-art on an overwhelming majority of these benchmarks. Finally, we demonstrate the generality of our algorithmic framework by instantiating it to the inclusion problem of Büchi pushdown automata into Büchi automata.

Subject Classification

ACM Subject Classification
  • Theory of computation → Formal languages and automata theory
Keywords
  • Büchi (Pushdown) Automata
  • ω-Language Inclusion
  • Well-quasiorders

Metrics

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

Supplementary Materials

References

  1. Parosh Aziz Abdulla, Yu-Fang Chen, Lorenzo Clemente, Lukáš Holík, Chih-Duo Hong, Richard Mayr, and Tomáš Vojnar. Simulation Subsumption in Ramsey-Based Büchi Automata Universality and Inclusion Testing. In Proc. Int. Conf. on Computer Aided Verification (CAV). Springer, 2010. URL: https://doi.org/10.1007/978-3-642-14295-6_14.
  2. Parosh Aziz Abdulla, Yu-Fang Chen, Lorenzo Clemente, Lukáš Holík, Chih-Duo Hong, Richard Mayr, and Tomáš Vojnar. Advanced Ramsey-Based Büchi Automata Inclusion Testing. In Proc. Int. Conf. on Concurrency Theory (CONCUR). Springer LNCS, 2011. URL: https://doi.org/10.1007/978-3-642-23217-6_13.
  3. Filippo Bonchi and Damien Pous. Checking NFA equivalence with bisimulations up to congruence. In Proc. of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). ACM, 2013. URL: https://doi.org/10.1145/2429069.2429124.
  4. Filippo Bonchi and Damien Pous. Hacking nondeterminism with induction and coinduction. Commun. ACM, 58(2), 2015. URL: https://doi.org/10.1145/2713167.
  5. Hugues Calbrix, Maurice Nivat, and Andreas Podelski. Ultimately periodic words of rational ω-languages. In Proc. Int. Symp. on Mathematical Foundations of Programming Semantics (MFPS), LNCS. Springer, 1994. URL: https://doi.org/10.1007/3-540-58027-1_27.
  6. Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem. Handbook of Model Checking. Springer, 1st edition, 2018. URL: https://doi.org/10.1007/978-3-319-10575-8.
  7. Lorenzo Clemente and Richard Mayr. Efficient reduction of nondeterministic automata with application to language inclusion testing. Logical Methods in Computer Science, 15(1), 2019. URL: https://doi.org/10.23638/LMCS-15(1:12)2019.
  8. Patrick Cousot and Radhia Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proc. 4th ACM Symp. on Principles of Programming Languages (POPL). ACM, 1977. URL: https://doi.org/10.1145/512950.512973.
  9. Patrick Cousot and Radhia Cousot. Systematic design of program analysis frameworks. In Proc. of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL). ACM, 1979. URL: https://doi.org/10.1145/567752.567778.
  10. K. Doveri, P. Ganty, F. Parolini, and F. Ranzato. BAIT: Büchi Automata Inclusion Tester. https://github.com/parof/bait, 2021.
  11. K. Doveri, P. Ganty, F. Parolini, and F. Ranzato. Büchi Automata benchmarks for language inclusion. https://github.com/parof/buchi-automata-benchmark, 2021.
  12. 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 Proc. 14th Int. Symp. on Automated Technology for Verification and Analysis (ATVA), LNCS. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-46520-3_8.
  13. Javier Esparza. Automata theory - An algorithmic approach. Lecture Notes, 2017. URL: https://www7.in.tum.de/~esparza/autoskript.pdf.
  14. Seth Fogarty and Moshe Y. Vardi. Efficient Büchi Universality Checking. In Proc. Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-12002-2_17.
  15. Pierre Ganty, Francesco Ranzato, and Pedro Valero. Language inclusion algorithms as complete abstract interpretations. In Proc. 26th Int. Static Analysis Symposium (SAS), LNCS. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-32304-2_8.
  16. Pierre Ganty, Francesco Ranzato, and Pedro Valero. Complete abstractions for checking language inclusion. ACM Trans. on Computational Logic, To appear, 2021. URL: http://arxiv.org/abs/1904.01388.
  17. Matthias Heizmann, Yu-Fang Chen, Daniel Dietsch, Marius Greitschus, Jochen Hoenicke, Yong Li, Alexander Nutz, Betim Musa, Christian Schilling, Tanja Schindler, and Andreas Podelski. Ultimate Automizer and the search for perfect interpolants - (competition contribution). In Proc. 24th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-89963-3_30.
  18. Matthias Heizmann, Jochen Hoenicke, and Andreas Podelski. Software model checking for people who love automata. In Proc. Int. Conf. on Computer Aided Verification (CAV). Springer LNCS, 2013. URL: https://doi.org/10.1007/978-3-642-39799-8_2.
  19. Philipp Hieronymi, Dun Ma, Reed Oei, Luke Schaeffer, Zhengyao Lin, Christian Schulz, and Jeffrey Shallit. Decidability for Sturmian words, 2021. URL: http://arxiv.org/abs/2102.08207.
  20. Martin Hofmann and Wei Chen. Abstract interpretation from Büchi automata. In Proc. of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). ACM Press, 2014. URL: https://doi.org/10.1145/2603088.2603127.
  21. Takumi Kasai and Shigeki Iwata. Some problems in formal language theory known as decidable are proved EXPTIME complete, 1992. URL: https://www.kurims.kyoto-u.ac.jp/~kyodo/kokyuroku/contents/pdf/0796-02.pdf.
  22. Bakhadyr Khoussainov and Nerode, Anil. Automata Theory and Its Applications. Springer, 2001. URL: https://doi.org/10.1007/978-1-4612-0171-7.
  23. Denis Kuperberg, Laureline Pinault, and Damien Pous. HKCω: Coinductive algorithms for Büchi automata. http://perso.ens-lyon.fr/damien.pous/covece/hkcw/, 2018.
  24. Denis Kuperberg, Laureline Pinault, and Damien Pous. Coinductive Algorithms for Büchi Automata. In Proc. Int. Conf. on Developments in Language Theory (DLT), LNCS. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-24886-4_15.
  25. Orna Kupferman. Automata Theory and Model Checking. In Handbook of Model Checking. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-10575-8_4.
  26. Orna Kupferman and Moshe Y. Vardi. Verification of fair transition systems. In Proc. Int. Conf. on Computer Aided Verification (CAV). Springer, 1996. URL: https://doi.org/10.1007/3-540-61474-5_84.
  27. Yong Li, Yu-Fang Chen, Lijun Zhang, and Depeng Liu. A novel learning algorithm for Büchi automata based on family of DFAs and classification trees. Information and Computation, 2020. URL: https://doi.org/10.1016/j.ic.2020.104678.
  28. Yong Li, Xuechao Sun, Andrea Turrini, Yu-Fang Chen, and Junnan Xu. ROLL 1.0: ω-regular language learning library. In Proc. 25th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-17462-0_23.
  29. Yong Li and Andrea Turini. Roll library: Regular Omega Language Learning library. https://github.com/ISCAS-PMC/roll-library, 2020.
  30. Yong Li, Andrea Turrini, Xuechao Sun, and Lijun Zhang. Proving non-inclusion of Büchi automata based on Monte Carlo sampling. In Proc. 14th Int. Symp. on Automated Technology for Verification and Analysis (ATVA). Springer, 2020. URL: https://doi.org/10.1007/978-3-030-59152-6_26.
  31. Oded Maler and Ludwig Staiger. On syntactic congruences for ω-languages. Technical report, Verimag, France, 2008. URL: http://www-verimag.imag.fr/~maler/Papers/congr.pdf.
  32. Roland Meyer, Sebastian Muskalla, and Elisabeth Neumann. Liveness verification and synthesis: New algorithms for recursive programs, 2017. URL: http://arxiv.org/abs/1701.02947.
  33. M. Michel. Complementation is more difficult with automata on infinite words. Technical report, CNET, Paris, 1988. Google Scholar
  34. Reed Oei, Dun Ma, Christian Schulz, and Philipp Hieronymi. Pecan: An automated theorem prover for automatic sequences using Büchi automata, 2021. URL: http://arxiv.org/abs/2102.01727.
  35. Dominique Perrin and Jean Eric Pin. Infinite Words: Automata, Semigroups, Logic and Games. Number 141 in Pure and Applied Mathematics Series. Elsevier, Amsterdam ; Boston, 1st edition, 2004. Google Scholar
  36. Nir Piterman. From nondeterministic Büchi and Streett automata to deterministic parity automata. Logical Methods in Computer Science, 3(3), 2007. URL: https://doi.org/10.2168/lmcs-3(3:5)2007.
  37. RABIT/Reduce: Tools for language inclusion testing and reduction of nondeterministic Büchi automata and NFA. http://www.languageinclusion.org/doku.php?id=tools. Accessed: 2021-01-29.
  38. Roman R. Redziejowski. An improved construction of deterministic omega-automaton using derivatives. Fundamenta Informaticae, 119(3–4), 2012. URL: https://doi.org/10.3233/FI-2012-744.
  39. Wolfgang Thomas. Languages, Automata, and Logic. In Handbook of Formal Languages: Volume 3 Beyond Words. Springer, 1997. URL: https://doi.org/10.1007/978-3-642-59126-6_7.
  40. Ming-Hsien Tsai, Seth Fogarty, Moshe Vardi, and Yih-Kuen Tsay. State of Büchi complementation. Logical Methods in Computer Science, 10(4), 2014. URL: https://doi.org/10.2168/lmcs-10(4:13)2014.
  41. Ming-Hsien Tsai, Yih-Kuen Tsay, and Yu-Shiang Hwang. GOAL for Games, Omega-Automata, and Logics. In Proc. Int. Conf. on Computer Aided Verification (CAV). Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39799-8_62.
  42. William M. Waite and Gerhard Goos. Compiler Construction. Springer-Verlag, New York, USA, 1984. 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