Document Open Access Logo

Singly Exponential Translation of Alternating Weak Büchi Automata to Unambiguous Büchi Automata

Authors Yong Li , Sven Schewe , Moshe Y. Vardi

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2023.37.pdf
  • Filesize: 0.84 MB
  • 17 pages

Document Identifiers

Author Details

Yong Li
  • University of Liverpool, UK
  • SKLCS, Institute of Software, Chinese Academy of Sciences, Beijing, China
Sven Schewe
  • University of Liverpool, UK
Moshe Y. Vardi
  • Rice University, Houston, TX, USA

Funding

This work has been supported in part by the EPSRC through grants EP/X021513/1 and EP/X017796/1, NSFC grant 62102407, NSF grants IIS-1527668, CCF-1704883, IIS-1830549, CNS-2016656, DoD MURI grant N00014-20-1-2787, and an award from the Maryland Procurement Office.

Acknowledgements

We thank the anonymous reviewers for their valuable feedback.

Cite As Get BibTex

Yong Li, Sven Schewe, and Moshe Y. Vardi. Singly Exponential Translation of Alternating Weak Büchi Automata to Unambiguous Büchi Automata. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 37:1-37:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.CONCUR.2023.37

Abstract

We introduce a method for translating an alternating weak Büchi automaton (AWA), which corresponds to a Linear Dynamic Logic (LDL) formula, to an unambiguous Büchi automaton (UBA). Our translations generalise constructions for Linear Temporal Logic (LTL), a less expressive specification language than LDL. In classical constructions, LTL formulas are first translated to alternating very weak automata (AVAs) - automata that have only singleton strongly connected components (SCCs); the AVAs are then handled by efficient disambiguation procedures. However, general AWAs can have larger SCCs, which complicates disambiguation. Currently, the only available disambiguation procedure has to go through an intermediate construction of nondeterministic Büchi automata (NBAs), which would incur an exponential blow-up of its own. We introduce a translation from general AWAs to UBAs with a singly exponential blow-up, which also immediately provides a singly exponential translation from LDL to UBAs. Interestingly, the complexity of our translation is smaller than the best known disambiguation algorithm for NBAs (broadly (0.53n)ⁿ vs. (0.76n)ⁿ), while the input of our construction can be exponentially more succinct.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automata over infinite objects
  • Theory of computation → Verification by model checking
Keywords
  • Büchi automata
  • unambiguous automata
  • alternation
  • weak
  • disambiguation

Metrics

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

Related Versions

References

  1. Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008. Google Scholar
  2. Christel Baier, Stefan Kiefer, Joachim Klein, Sascha Klüppelholz, David Müller, and James Worrell. Markov chains and unambiguous Büchi automata. In Swarat Chaudhuri and Azadeh Farzan, editors, Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I, volume 9779 of Lecture Notes in Computer Science, pages 23-42. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-41528-4_2.
  3. J.P. Barthelemy. An asymptotic equivalent for the number of total preorders on a finite set. Discrete Mathematics, 29(3):311-313, 1980. URL: https://doi.org/10.1016/0012-365X(80)90159-4.
  4. Michael Benedikt, Rastislav Lenhardt, and James Worrell. LTL model checking of interval markov chains. In Nir Piterman and Scott A. Smolka, editors, Tools and Algorithms for the Construction and Analysis of Systems - 19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings, volume 7795 of Lecture Notes in Computer Science, pages 32-46. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-36742-7_3.
  5. Frantisek Blahoudek, Juraj Major, and Jan Strejcek. LTL to smaller self-loop alternating automata and back. In Robert M. Hierons and Mohamed Mosbah, editors, Theoretical Aspects of Computing - ICTAC 2019 - 16th International Colloquium, Hammamet, Tunisia, October 31 - November 4, 2019, Proceedings, volume 11884 of Lecture Notes in Computer Science, pages 152-171. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-32505-3_10.
  6. Udi Boker, Orna Kupferman, and Adin Rosenberg. Alternation removal in Büchi automata. In Samson Abramsky, Cyril Gavoille, Claude Kirchner, Friedhelm Meyer auf der Heide, and Paul G. Spirakis, editors, Automata, Languages and Programming, 37th International Colloquium, ICALP 2010, Bordeaux, France, July 6-10, 2010, Proceedings, Part II, volume 6199 of Lecture Notes in Computer Science, pages 76-87. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-14162-1_7.
  7. Udi Boker, Karoliina Lehtinen, and Salomon Sickert. On the translation of automata to linear temporal logic. In Patricia Bouyer and Lutz Schröder, editors, Foundations of Software Science and Computation Structures - 25th International Conference, FOSSACS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, volume 13242 of Lecture Notes in Computer Science, pages 140-160. Springer, 2022. URL: https://doi.org/10.1007/978-3-030-99253-8_8.
  8. J. Richard Büchi. On a decision method in restricted second order arithmetic. In Proc. Int. Congress on Logic, Method, and Philosophy of Science. 1960, pages 1-12. Stanford University Press, 1962. Google Scholar
  9. Doron Bustan, Sasha Rubin, and Moshe Y. Vardi. Verifying omega-regular properties of Markov chains. In Rajeev Alur and Doron A. Peled, editors, Computer Aided Verification, 16th International Conference, CAV 2004, Boston, MA, USA, July 13-17, 2004, Proceedings, volume 3114 of Lecture Notes in Computer Science, pages 189-201. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-27813-9_15.
  10. Olivier Carton and Max Michel. Unambiguous Büchi automata. Theor. Comput. Sci., 297(1-3):37-81, 2003. URL: https://doi.org/10.1016/S0304-3975(02)00618-7.
  11. Paul Gastin and Denis Oddoux. Fast LTL to Büchi automata translation. In Gérard Berry, Hubert Comon, and Alain Finkel, editors, Computer Aided Verification, 13th International Conference, CAV 2001, Paris, France, July 18-22, 2001, Proceedings, volume 2102 of Lecture Notes in Computer Science, pages 53-65. Springer, 2001. URL: https://doi.org/10.1007/3-540-44585-4_6.
  12. Giuseppe De Giacomo and Moshe Y. Vardi. Linear temporal logic and linear dynamic logic on finite traces. In Francesca Rossi, editor, IJCAI 2013, Proceedings of the 23rd International Joint Conference on Artificial Intelligence, Beijing, China, August 3-9, 2013, pages 854-860. IJCAI/AAAI, 2013. URL: http://www.aaai.org/ocs/index.php/IJCAI/IJCAI13/paper/view/6997.
  13. Gerard J. Holzmann. The model checker SPIN. IEEE Trans. Software Eng., 23(5):279-295, 1997. URL: https://doi.org/10.1109/32.588521.
  14. Simon Jantsch, David Müller, Christel Baier, and Joachim Klein. From LTL to unambiguous Büchi automata via disambiguation of alternating automata. Formal Methods Syst. Des., 58(1-2):42-82, 2021. URL: https://doi.org/10.1007/s10703-021-00379-z.
  15. Detlef Kähler and Thomas Wilke. Complementation, disambiguation, and determinization of Büchi automata unified. In Luca Aceto, Ivan Damgård, Leslie Ann Goldberg, Magnús M. Halldórsson, Anna Ingólfsdóttir, and Igor Walukiewicz, editors, Automata, Languages and Programming, 35th International Colloquium, ICALP 2008, Reykjavik, Iceland, July 7-11, 2008, Proceedings, Part I: Tack A: Algorithms, Automata, Complexity, and Games, volume 5125 of Lecture Notes in Computer Science, pages 724-735. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-70575-8_59.
  16. Hrishikesh Karmarkar, Manas Joglekar, and Supratik Chakraborty. Improved upper and lower bounds for Büchi disambiguation. In Dang Van Hung and Mizuhito Ogawa, editors, Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013, Hanoi, Vietnam, October 15-18, 2013. Proceedings, volume 8172 of Lecture Notes in Computer Science, pages 40-54. Springer, 2013. URL: https://doi.org/10.1007/978-3-319-02444-8_5.
  17. 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.
  18. Marta Z. Kwiatkowska, Gethin Norman, and David Parker. PRISM 4.0: Verification of probabilistic real-time systems. In Ganesh Gopalakrishnan and Shaz Qadeer, editors, Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, volume 6806 of Lecture Notes in Computer Science, pages 585-591. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-22110-1_47.
  19. Yong Li, Sven Schewe, and Moshe Y. Vardi. Singly exponential translation of alternating weak büchi automata to unambiguous büchi automata. CoRR, abs/2305.09966, 2023. URL: https://doi.org/10.48550/arXiv.2305.09966.
  20. 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.
  21. David E. Muller, Ahmed Saoudi, and Paul E. Schupp. Alternating automata, the weak monadic theory of trees and its complexity. Theor. Comput. Sci., 97(2):233-244, 1992. URL: https://doi.org/10.1016/0304-3975(92)90076-R.
  22. David E. Muller and Paul E. Schupp. Alternating automata on infinite objects, determinacy and rabin’s theorem. In Maurice Nivat and Dominique Perrin, editors, Automata on Infinite Words, Ecole de Printemps d'Informatique Théorique, Le Mont Dore, France, May 14-18, 1984, volume 192 of Lecture Notes in Computer Science, pages 100-107. Springer, 1984. URL: https://doi.org/10.1007/3-540-15641-0_27.
  23. Gareth Scott Rohde. Alternating automata and the temporal logic of ordinals. PhD thesis, University of Illinois at Urbana-Champaign, 1997. Google Scholar
  24. 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 für Informatik, Germany, 2009. URL: https://doi.org/10.4230/LIPIcs.STACS.2009.1854.
  25. Moshe Y. Vardi. The rise and fall of LTL. In Giovanna D'Agostino and Salvatore La Torre, editors, Proceedings of Second International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2011, Minori, Italy, 15-17th June 2011, 2011. invited talk. URL: https://www.cs.rice.edu/~vardi/papers/gandalf11-myv.pdf.
  26. Moshe Y. Vardi and Pierre Wolper. An automata-theoretic approach to automatic program verification (preliminary report). In Proceedings of the Symposium on Logic in Computer Science (LICS '86), Cambridge, Massachusetts, USA, June 16-18, 1986, pages 332-344. IEEE Computer Society, 1986. 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 About DROPS Imprint Privacy Contact