Singly exponential translation of alternating weak Büchi automata to unambiguous Büchi automata. (English) Zbl 07871734
Summary: 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 generalize 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 Büchi automata (AVAs) – automata that have only singleton strongly connected components (SCCs); these 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)^n\) vs. \((0.76 n)^n\)), while the input of our construction can be exponentially more succinct.
MSC:
| 68Qxx | Theory of computing |
References:
| [1] | Büchi, J. R., On a decision method in restricted second order arithmetic, (Proc. Int. Congress on Logic, Method, and Philosophy of Science. 1960, 1962, Stanford University Press), 1-12 · Zbl 0147.25103 |
| [2] | Vardi, M. Y.; Wolper, P., An automata-theoretic approach to automatic program verification (preliminary report), (Proceedings of the Symposium on Logic in Computer Science (LICS ’86). Proceedings of the Symposium on Logic in Computer Science (LICS ’86), June 16-18, 1986, 1986, IEEE Computer Society: IEEE Computer Society Cambridge, Massachusetts, USA), 332-344 |
| [3] | Holzmann, G. J., The model checker SPIN, IEEE Trans. Softw. Eng., 23, 5, 279-295, 1997 |
| [4] | Gastin, P.; Oddoux, D., Fast LTL to Büchi automata translation, (Berry, G.; Comon, H.; Finkel, A., Computer Aided Verification, 13th International Conference, Proceedings. Computer Aided Verification, 13th International Conference, Proceedings, CAV 2001, Paris, France, July 18-22, 2001. Computer Aided Verification, 13th International Conference, Proceedings. Computer Aided Verification, 13th International Conference, Proceedings, CAV 2001, Paris, France, July 18-22, 2001, Lecture Notes in Computer Science, vol. 2102, 2001, Springer), 53-65 · Zbl 0991.68044 |
| [5] | Baier, C.; Katoen, J., Principles of Model Checking, 2008, MIT Press · Zbl 1179.68076 |
| [6] | Muller, D. E.; Schupp, P. E., Alternating automata on infinite objects, determinacy and Rabin’s theorem, (Nivat, M.; Perrin, D., Automata on Infinite Words. Automata on Infinite Words, Ecole de Printemps d’Informatique Théorique, Le Mont Dore, France, May 14-18, 1984. Automata on Infinite Words. Automata on Infinite Words, Ecole de Printemps d’Informatique Théorique, Le Mont Dore, France, May 14-18, 1984, Lecture Notes in Computer Science, vol. 192, 1984, Springer), 100-107 · Zbl 0608.03004 |
| [7] | Miyano, S.; Hayashi, T., Alternating finite automata on omega-words, Theor. Comput. Sci., 32, 321-330, 1984 · Zbl 0544.68042 |
| [8] | Boker, U.; Kupferman, O.; Rosenberg, A., Alternation removal in Büchi automata, (Abramsky, S.; Gavoille, C.; Kirchner, C.; auf der Heide, F. M.; Spirakis, P. G., Automata, Languages and Programming, 37th International Colloquium, Proceedings, Part II. Automata, Languages and Programming, 37th International Colloquium, Proceedings, Part II, ICALP 2010, Bordeaux, France, July 6-10, 2010. Automata, Languages and Programming, 37th International Colloquium, Proceedings, Part II. Automata, Languages and Programming, 37th International Colloquium, Proceedings, Part II, ICALP 2010, Bordeaux, France, July 6-10, 2010, Lecture Notes in Computer Science, vol. 6199, 2010, Springer), 76-87 · Zbl 1288.68148 |
| [9] | Vardi, M. Y., The rise and fall of LTL, (D’Agostino, G.; Torre, S. L., Proceedings of Second International Symposium on Games, Automata, Logics and Formal Verification. Proceedings of Second International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2011, Minori, Italy, 15-17th June, 2011, 2011), invited talk |
| [10] | Giacomo, G. D.; Vardi, M. Y., Linear temporal logic and linear dynamic logic on finite traces, (Rossi, F., IJCAI 2013, Proceedings of the 23rd International Joint Conference on Artificial Intelligence. IJCAI 2013, Proceedings of the 23rd International Joint Conference on Artificial Intelligence, Beijing, China, August 3-9, 2013, IJCAI/AAAI, 2013), 854-860 |
| [11] | Kupferman, O.; Vardi, M. Y., Weak alternating automata are not that weak, ACM Trans. Comput. Log., 2, 3, 408-429, 2001 · Zbl 1171.68551 |
| [12] | Blahoudek, F.; Major, J.; Strejcek, J., LTL to smaller self-loop alternating automata and back, (Hierons, R. M.; Mosbah, M., Theoretical Aspects of Computing - ICTAC 2019 - 16th International Colloquium, Proceedings. Theoretical Aspects of Computing - ICTAC 2019 - 16th International Colloquium, Proceedings, Hammamet, Tunisia, October 31 - November 4, 2019. Theoretical Aspects of Computing - ICTAC 2019 - 16th International Colloquium, Proceedings. Theoretical Aspects of Computing - ICTAC 2019 - 16th International Colloquium, Proceedings, Hammamet, Tunisia, October 31 - November 4, 2019, Lecture Notes in Computer Science, vol. 11884, 2019, Springer), 152-171 · Zbl 1425.68012 |
| [13] | Boker, U.; Lehtinen, K.; Sickert, S., On the translation of automata to linear temporal logic, (Bouyer, P.; Schröder, L., 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, Proceedings. 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, Proceedings, ETAPS 2022, Munich, Germany, April 2-7, 2022. 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, Proceedings. 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, Proceedings, ETAPS 2022, Munich, Germany, April 2-7, 2022, Lecture Notes in Computer Science, vol. 13242, 2022, Springer), 140-160 · Zbl 1528.68019 |
| [14] | Rohde, G. S., Alternating automata and the temporal logic of ordinals, 1997, University of Illinois at Urbana-Champaign, Ph.D. thesis |
| [15] | Carton, O.; Michel, M., Unambiguous Büchi automata, Theor. Comput. Sci., 297, 1-3, 37-81, 2003 · Zbl 1044.68084 |
| [16] | Baier, C.; Kiefer, S.; Klein, J.; Müller, D.; Worrell, J., Markov chains and unambiguous automata, J. Comput. Syst. Sci., 136, 113-134, 2023 · Zbl 07695012 |
| [17] | Bustan, D.; Rubin, S.; Vardi, M. Y., Verifying omega-regular properties of Markov chains, (Alur, R.; Peled, D. A., Computer Aided Verification, 16th International Conference, Proceedings. Computer Aided Verification, 16th International Conference, Proceedings, CAV 2004, Boston, MA, USA, July 13-17, 2004. Computer Aided Verification, 16th International Conference, Proceedings. Computer Aided Verification, 16th International Conference, Proceedings, CAV 2004, Boston, MA, USA, July 13-17, 2004, Lecture Notes in Computer Science, vol. 3114, 2004, Springer), 189-201 · Zbl 1103.68072 |
| [18] | Kwiatkowska, M. Z.; Norman, G.; Parker, D., PRISM 4.0: verification of probabilistic real-time systems, (Gopalakrishnan, G.; Qadeer, S., Computer Aided Verification - 23rd International Conference, Proceedings. Computer Aided Verification - 23rd International Conference, Proceedings, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Computer Aided Verification - 23rd International Conference, Proceedings. Computer Aided Verification - 23rd International Conference, Proceedings, CAV 2011, Snowbird, UT, USA, July 14-20, 2011, Lecture Notes in Computer Science, vol. 6806, 2011, Springer), 585-591 |
| [19] | Löding, C., Unambiguous finite automata, (Béal, M.; Carton, O., Developments in Language Theory - 17th International Conference, Proceedings. Developments in Language Theory - 17th International Conference, Proceedings, DLT 2013, Marne-la-Vallée, France, June 18-21, 2013. Developments in Language Theory - 17th International Conference, Proceedings. Developments in Language Theory - 17th International Conference, Proceedings, DLT 2013, Marne-la-Vallée, France, June 18-21, 2013, Lecture Notes in Computer Science, vol. 7907, 2013, Springer), 29-30 |
| [20] | Colcombet, T.; Quaas, K.; Skrzypczak, M., Unambiguity in automata theory, Dagstuhl Seminar 21452. Dagstuhl Seminar 21452, Dagstuhl Rep., 11, 10, 57-71, 2021 |
| [21] | Stearns, R. E.; Iii, H. B.H., On the equivalence and containment problems for unambiguous regular expressions, regular grammars and finite automata, SIAM J. Comput., 14, 3, 598-611, 1985 · Zbl 0577.68074 |
| [22] | Jr., J. J.; Jirásková, G.; Sebej, J., Operations on unambiguous finite automata, Int. J. Found. Comput. Sci., 29, 5, 861-876, 2018 · Zbl 1403.68115 |
| [23] | Indzhev, E.; Kiefer, S., On complementing unambiguous automata and graphs with many cliques and cocliques, Inf. Process. Lett., 177, Article 106270 pp., 2022 · Zbl 07537429 |
| [24] | Rabinovich, A., Complementation of finitely ambiguous Büchi automata, (Hoshi, M.; Seki, S., DLT. DLT, LNCS, vol. 11088, 2018, Springer), 541-552 · Zbl 1457.68148 |
| [25] | Feng, W.; Li, Y.; Turrini, A.; Vardi, M. Y.; Zhang, L., On the power of finite ambiguity in Büchi complementation, Inf. Comput., 292, Article 105032 pp., 2023 · Zbl 07687219 |
| [26] | Benedikt, M.; Lenhardt, R.; Worrell, J., LTL model checking of interval Markov chains, (Piterman, N.; Smolka, S. A., 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, Proceedings. 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, Proceedings, ETAPS 2013, Rome, Italy, March 16-24, 2013. 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, Proceedings. 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, Proceedings, ETAPS 2013, Rome, Italy, March 16-24, 2013, Lecture Notes in Computer Science, vol. 7795, 2013, Springer), 32-46 · Zbl 1381.68147 |
| [27] | Jantsch, S.; Müller, D.; Baier, C.; Klein, J., From LTL to unambiguous Büchi automata via disambiguation of alternating automata, Form. Methods Syst. Des., 58, 1-2, 42-82, 2021 · Zbl 1505.68022 |
| [28] | Barthelemy, J., An asymptotic equivalent for the number of total preorders on a finite set, Discrete Math., 29, 3, 311-313, 1980 · Zbl 0445.05011 |
| [29] | Karmarkar, H.; Joglekar, M.; Chakraborty, S., Improved upper and lower bounds for Büchi disambiguation, (Hung, D. V.; Ogawa, M., Automated Technology for Verification and Analysis - 11th International Symposium, Proceedings. Automated Technology for Verification and Analysis - 11th International Symposium, Proceedings, ATVA 2013, Hanoi, Vietnam, October 15-18, 2013. Automated Technology for Verification and Analysis - 11th International Symposium, Proceedings. Automated Technology for Verification and Analysis - 11th International Symposium, Proceedings, ATVA 2013, Hanoi, Vietnam, October 15-18, 2013, Lecture Notes in Computer Science, vol. 8172, 2013, Springer), 40-54 · Zbl 1410.68206 |
| [30] | Schewe, S., Büchi complementation made tight, (Albers, S.; Marion, J., 26th International Symposium on Theoretical Aspects of Computer Science, Proceedings. 26th International Symposium on Theoretical Aspects of Computer Science, Proceedings, STACS 2009, February 26-28, 2009, Freiburg, Germany. 26th International Symposium on Theoretical Aspects of Computer Science, Proceedings. 26th International Symposium on Theoretical Aspects of Computer Science, Proceedings, STACS 2009, February 26-28, 2009, Freiburg, Germany, LIPIcs, vol. 3, 2009, Schloss Dagstuhl - Leibniz-Zentrum für Informatik: Schloss Dagstuhl - Leibniz-Zentrum für Informatik Germany), 661-672 · Zbl 1236.68176 |
| [31] | Leung, H., Descriptional complexity of NFA of different ambiguity, Int. J. Found. Comput. Sci., 16, 5, 975-984, 2005 · Zbl 1090.68059 |
| [32] | Kähler, D.; Wilke, T., Complementation, disambiguation, and determinization of Büchi automata unified, (Aceto, L.; Damgård, I.; Goldberg, L. A.; Halldórsson, M. M.; Ingólfsdóttir, A.; Walukiewicz, I., Automata, Languages and Programming, 35th International Colloquium, Proceedings, Part I: Tack A: Algorithms, Automata, Complexity, and Games. Automata, Languages and Programming, 35th International Colloquium, Proceedings, Part I: Tack A: Algorithms, Automata, Complexity, and Games, ICALP 2008, Reykjavik, Iceland, July 7-11, 2008. Automata, Languages and Programming, 35th International Colloquium, Proceedings, Part I: Tack A: Algorithms, Automata, Complexity, and Games. Automata, Languages and Programming, 35th International Colloquium, Proceedings, Part I: Tack A: Algorithms, Automata, Complexity, and Games, ICALP 2008, Reykjavik, Iceland, July 7-11, 2008, Lecture Notes in Computer Science, vol. 5125, 2008, Springer), 724-735 · Zbl 1153.68032 |
| [33] | Li, Y.; Schewe, S.; Vardi, M. Y., Singly exponential translation of alternating weak Büchi automata to unambiguous Büchi automata, (Pérez, G. A.; Raskin, J., 34th International Conference on Concurrency Theory. 34th International Conference on Concurrency Theory, CONCUR 2023, September 18-23, 2023, Antwerp, Belgium. 34th International Conference on Concurrency Theory. 34th International Conference on Concurrency Theory, CONCUR 2023, September 18-23, 2023, Antwerp, Belgium, LIPIcs, vol. 279, 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik), 37:1-37:17 |
| [34] | Muller, D. E.; Saoudi, A.; Schupp, P. E., Alternating automata, the weak monadic theory of trees and its complexity, Theor. Comput. Sci., 97, 2, 233-244, 1992 · Zbl 0776.03017 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
