Document Open Access Logo

Reducing Acceptance Marks in Emerson-Lei Automata by QBF Solving

Authors Tereza Schwarzová , Jan Strejček , Juraj Major

PDF
Thumbnail PDF

File

LIPIcs.SAT.2023.23.pdf
  • Filesize: 0.86 MB
  • 20 pages

Document Identifiers

Author Details

Tereza Schwarzová
  • Masaryk University, Brno, Czech Republic
Jan Strejček
  • Masaryk University, Brno, Czech Republic
Juraj Major
  • Masaryk University, Brno, Czech Republic

Funding

T. Schwarzová received funding from the European Union’s Horizon Europe program under the Grant Agreement No. 101087529.

Cite As Get BibTex

Tereza Schwarzová, Jan Strejček, and Juraj Major. Reducing Acceptance Marks in Emerson-Lei Automata by QBF Solving. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 23:1-23:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.SAT.2023.23

Abstract

This paper presents a novel application of QBF solving to automata reduction. We focus on Transition-based Emerson-Lei automata (TELA), which is a popular formalism that generalizes many traditional kinds of automata over infinite words including Büchi, co-Büchi, Rabin, Streett, and parity automata. Transitions in a TELA are labelled with acceptance marks and its accepting formula is a positive Boolean combination of atoms saying that a particular mark has to be visited infinitely or finitely often. Algorithms processing these automata are often very sensitive to the number of acceptance marks. We introduce a new technique for reducing the number of acceptance marks in TELA based on satisfiability of quantified Boolean formulas (QBF). We evaluated our reduction technique on TELA produced by state-of-the-art tools of the libraries Owl and Spot and by the tool ltl3tela. The technique reduced some acceptance marks in automata produced by all the tools. On automata with more than one acceptance mark obtained by translation of LTL formulas from literature with tools Delag and Rabinizer 4, our technique reduced 27.7% and 39.3% of acceptance marks, respectively. The reduction was even higher on automata from random formulas.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
  • Theory of computation → Automata over infinite objects
Keywords
  • Emerson-Lei automata
  • TELA
  • automata reduction
  • QBF
  • telatko

Metrics

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

Supplementary Materials

References

  1. Souheib Baarir and Alexandre Duret-Lutz. Mechanizing the minimization of deterministic generalized Büchi automata. In Proceedings of the 34th IFIP International Conference on Formal Techniques for Distributed Objects, Components and Systems (FORTE'14), volume 8461 of Lecture Notes in Computer Science, pages 266-283. Springer, June 2014. URL: https://doi.org/10.1007/978-3-662-43613-4_17.
  2. Souheib Baarir and Alexandre Duret-Lutz. SAT-based minimization of deterministic ω-automata. In Martin Davis, Ansgar Fehnker, Annabelle McIver, and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR 2015, Suva, Fiji, November 24-28, 2015, Proceedings, volume 9450 of Lecture Notes in Computer Science, pages 79-87. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-48899-7_6.
  3. 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 Proceedings of the 27th Conference on Computer Aided Verification (CAV'15), volume 8172 of Lecture Notes in Computer Science, pages 442-445. Springer, 2015. See also URL: http://adl.github.io/hoaf/.
  4. Tomáš Babiak, Thomas Badie, Alexandre Duret-Lutz, Mojmír Křetínský, and Jan Strejček. Compositional approach to suspension and other improvements to LTL translation. In Ezio Bartocci and C. R. Ramakrishnan, editors, Model Checking Software - 20th International Symposium, SPIN 2013, Stony Brook, NY, USA, July 8-9, 2013. Proceedings, volume 7976 of Lecture Notes in Computer Science, pages 81-98. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39176-7_6.
  5. 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 Proceedings of the 17th International Symposium on Automated Technology for Verification and Analysis (ATVA'19), volume 11781 of Lecture Notes in Computer Science, pages 445-461. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-31784-3_26.
  6. Antonio Casares, Thomas Colcombet, and Nathanaël Fijalkow. Optimal transformations of games and automata using muller conditions. In Nikhil Bansal, Emanuela Merelli, and James Worrell, editors, 48th International Colloquium on Automata, Languages, and Programming, ICALP 2021, July 12-16, 2021, Glasgow, Scotland (Virtual Conference), volume 198 of LIPIcs, pages 123:1-123:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.ICALP.2021.123.
  7. Antonio Casares, Alexandre Duret-Lutz, Klara J. Meyer, Florian Renkin, and Salomon Sickert. Practical applications of the Alternating Cycle Decomposition. In Dana Fisman and Grigore Rosu, editors, Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part II, volume 13244 of Lecture Notes in Computer Science, pages 99-117. Springer, 2022. URL: https://doi.org/10.1007/978-3-030-99527-0_6.
  8. Leonardo Mendonça de Moura and Nikolaj Bjørner. Z3: an efficient SMT solver. In C. R. Ramakrishnan and Jakob Rehof, editors, Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, volume 4963 of Lecture Notes in Computer Science, pages 337-340. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-78800-3_24.
  9. 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 Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis (ATVA'16), volume 9938 of Lecture Notes in Computer Science, pages 122-129. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-46520-3_8.
  10. Rüdiger Ehlers. Minimising deterministic Büchi automata precisely using SAT solving. In O. Strichman and S. Szeider, editors, Proceedings of the 13th International Conference on Theory and Applications of Satisfiability Testing (SAT'10), volume 6175 of Lecture Notes in Computer Science, pages 326-332. Springer, 2010. Google Scholar
  11. Rüdiger Ehlers and Bernd Finkbeiner. On the virtue of patience: Minimizing Büchi automata. In Jaco van de Pol and Michael Weber, editors, Model Checking Software - 17th International SPIN Workshop, Enschede, The Netherlands, September 27-29, 2010. Proceedings, volume 6349 of Lecture Notes in Computer Science, pages 129-145. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-16164-3_10.
  12. E. Allen Emerson and Chin-Laung Lei. Modalities for model checking: Branching time logic strikes back. Science of Computer Programming, 8(3):275-306, June 1987. Google Scholar
  13. Jan Křetínský, Tobias Meggendorfer, Salomon Sickert, and Christopher Ziegler. Rabinizer 4: From LTL to your favourite deterministic automaton. In Hana Chockler and Georg Weissenbacher, editors, Proceedings of the 30th International Conference on Computer Aided Verification (CAV'18), volume 10981 of Lecture Notes in Computer Science, pages 567-577. Springer, 2018. Google Scholar
  14. Jan Křetínský, Tobias Meggendorfer, and Salomon Sickert. Owl: A library for ω-words, automata, and LTL. In Shuvendu K. Lahiri and Chao Wang, editors, Automated Technology for Verification and Analysis - 16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings, volume 11138 of Lecture Notes in Computer Science, pages 543-550. Springer, 2018. URL: https://doi.org/10.1007/978-3-030-01090-4_34.
  15. Juraj Major, František Blahoudek, Jan Strejček, Miriama Sasaráková, and Tatiana Zbončáková. ltl3tela: LTL to small deterministic or nondeterministic Emerson-Lei automata. In Yu-Fang Chen, Chih-Hong Cheng, and Javier Esparza, editors, Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings, volume 11781 of Lecture Notes in Computer Science, pages 357-365. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-31784-3_21.
  16. David Müller and Salomon Sickert. LTL to deterministic Emerson-Lei automata. In Patricia Bouyer, Andrea Orlandini, and Pierluigi San Pietro, editors, Proceedings of the Eighth International Symposium on Games, Automata, Logics and Formal Verification (GandALF'17), volume 256 of EPTCS, pages 180-194, September 2017. Google Scholar
  17. Amir Pnueli. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1 November 1977, pages 46-57. IEEE Computer Society, 1977. URL: https://doi.org/10.1109/SFCS.1977.32.
  18. Florian Renkin, Alexandre Duret-Lutz, and Adrien Pommellet. Practical "paritizing" of Emerson-Lei automata. In Dang Van Hung and Oleg Sokolsky, editors, Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Hanoi, Vietnam, October 19-23, 2020, Proceedings, volume 12302 of Lecture Notes in Computer Science, pages 127-143. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-59152-6_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-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact