Determinization and limit-determinization of Emerson-Lei automata. (English) Zbl 1497.68270
Hou, Zhe (ed.) et al., Automated technology for verification and analysis. 19th international symposium, ATVA 2021, Gold Coast, QLD, Australia, October 18–22, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12971, 15-31 (2021).
Summary: We study the problem of determinizing \(\omega \)-automata whose acceptance condition is defined on the transitions using Boolean formulas, also known as transition-based Emerson-Lei automata (TELA). The standard approach to determinize TELA first constructs an equivalent generalized Büchi automaton (GBA), which is later determinized. We introduce three new ways of translating TELA to GBA. Furthermore, we give a new determinization construction which determinizes several GBA separately and combines them using a product construction. An experimental evaluation shows that the product approach is competitive when compared with state-of-the-art determinization procedures. We also study limit-determinization of TELA and show that this can be done with a single-exponential blow-up, in contrast to the known double-exponential lower-bound for determinization. Finally, one version of the limit-determinization procedure yields good-for-MDP automata which can be used for quantitative probabilistic model checking.
For the entire collection see [Zbl 1489.68022].
For the entire collection see [Zbl 1489.68022].
MSC:
| 68Q45 | Formal languages and automata |
References:
| [1] | Babiak, T.; Kroening, D.; Păsăreanu, CS, The Hanoi omega-automata format, Computer Aided Verification, 479-486 (2015), Cham: Springer, Cham · doi:10.1007/978-3-319-21690-4_31 |
| [2] | Baier, C.; Blahoudek, F.; Duret-Lutz, A.; Klein, J.; Müller, D.; Strejček, J.; Chen, Y-F; Cheng, C-H; Esparza, J., Generic emptiness check for fun and profit, Automated Technology for Verification and Analysis, 445-461 (2019), Cham: Springer, Cham · Zbl 1437.68092 · doi:10.1007/978-3-030-31784-3_26 |
| [3] | Baier, C.; Katoen, JP, Principles of Model Checking (2008), Cambridge: The MIT Press, Cambridge · Zbl 1179.68076 |
| [4] | Ben-Ari, M., Principles of the Spin Model Checker (2008), London: Springer, London · Zbl 1142.68044 · doi:10.1007/978-1-84628-770-1 |
| [5] | Blahoudek, F.: Automata for formal methods: little steps towards perfection. Ph.D. thesis, Masaryk University, Faculty of Informatics (2018) |
| [6] | Blahoudek, F., Duret-Lutz, A., Klokocka, M., Kretínský, M., Strejcek, J.: Seminator: a tool for semi-determinization of omega-automata. In: International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR). EPiC Series in Computing (2017) |
| [7] | Blahoudek, F.; Major, J.; Strejček, J.; Hierons, RM; Mosbah, M., LTL to smaller self-loop alternating automata and back, Theoretical Aspects of Computing - ICTAC 2019, 152-171 (2019), Cham: Springer, Cham · Zbl 1539.68132 · doi:10.1007/978-3-030-32505-3_10 |
| [8] | Bloemen, V.; Duret-Lutz, A.; van de Pol, J., Model checking with generalized Rabin and Fin-less automata, Int. J. Softw. Tools Technol. Transfer, 21, 3, 307-324 (2019) · doi:10.1007/s10009-019-00508-4 |
| [9] | Boker, U.: Why these automata types? In: Logic for Programming, Artificial Intelligence and Reasoning (LPAR). EPiC Series in Computing (2018) |
| [10] | Chatterjee, K.; Gaiser, A.; Křetínský, J.; Sharygina, N.; Veith, H., Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis, Computer Aided Verification, 559-575 (2013), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-642-39799-8_37 |
| [11] | Courcoubetis, C.; Yannakakis, M., The complexity of probabilistic verification, J. ACM, 42, 4, 857-907 (1995) · Zbl 0885.68109 · doi:10.1145/210332.210339 |
| [12] | Couvreur, J-M; Wing, JM; Woodcock, J.; Davies, J., On-the-fly verification of linear temporal logic, FM’99 — Formal Methods, 253-271 (1999), Heidelberg: Springer, Heidelberg · Zbl 0954.68102 · doi:10.1007/3-540-48119-2_16 |
| [13] | Duret-Lutz, A.: Contributions to LTL and \(\omega \)-automata for model checking. Habilitation thesis, Université Pierre et Marie Curie (2017) |
| [14] | Duret-Lutz, A.; Lewkowicz, A.; Fauchille, A.; Michaud, T.; Renault, É.; Xu, L.; Artho, C.; Legay, A.; Peled, D., Spot 2.0—a framework for LTL and \(\omega \)-automata manipulation, Automated Technology for Verification and Analysis, 122-129 (2016), Cham: Springer, Cham · doi:10.1007/978-3-319-46520-3_8 |
| [15] | Duret-Lutz, A.; Poitrenaud, D.; Couvreur, J-M; Liu, Z.; Ravn, AP, On-the-fly emptiness check of transition-based Streett automata, Automated Technology for Verification and Analysis, 213-227 (2009), Heidelberg: Springer, Heidelberg · Zbl 1262.68118 · doi:10.1007/978-3-642-04761-9_17 |
| [16] | Emerson, EA; Lei, CL, Modalities for model checking: branching time logic strikes back, Sci. Comput. Program., 8, 3, 275-306 (1987) · Zbl 0615.68019 · doi:10.1016/0167-6423(87)90036-0 |
| [17] | Esparza, J., Křetínský, J., Sickert, S.: One theorem to rule them all: a unified translation of LTL into \(\omega \)-automata. In: Logic in Computer Science (LICS). ACM (2018) · Zbl 1497.68259 |
| [18] | Giannakopoulou, D.; Lerda, F.; Peled, DA; Vardi, MY, From states to transitions: improving translation of LTL formulae to Büchi automata, Formal Techniques for Networked and Distributed Sytems — FORTE 2002, 308-326 (2002), Heidelberg: Springer, Heidelberg · Zbl 1037.68553 · doi:10.1007/3-540-36135-9_20 |
| [19] | Hahn, E.M., Li, G., Schewe, S., Turrini, A., Zhang, L.: Lazy probabilistic model checking without determinisation. In: Concurrency Theory (CONCUR) (2015) · Zbl 1374.68290 |
| [20] | Hahn, EM; Perez, M.; Schewe, S.; Somenzi, F.; Trivedi, A.; Wojtczak, D.; Biere, A.; Parker, D., Good-for-MDPs automata for probabilistic analysis and reinforcement learning, Tools and Algorithms for the Construction and Analysis of Systems, 306-323 (2020), Cham: Springer, Cham · Zbl 1507.68167 · doi:10.1007/978-3-030-45190-5_17 |
| [21] | John, T., Jantsch, S., Baier, C., Klüppelholz, S.: Determinization and limit-determinization of Emerson-Lei automata. arXiv:2106.15892 [cs], June 2021 |
| [22] | John, T., Jantsch, S., Baier, C., Klüppelholz, S.: Determinization and limit-determinization of Emerson-Lei automata. Supplementary material (ATVA 2021) (2021). doi:10.6084/m9.figshare.14838654.v2 |
| [23] | Klein, J.; Müller, D.; Baier, C.; Klüppelholz, S.; Dediu, A-H; Martín-Vide, C.; Sierra-Rodríguez, J-L; Truthe, B., Are good-for-games automata good for probabilistic model checking?, Language and Automata Theory and Applications, 453-465 (2014), Cham: Springer, Cham · Zbl 1408.68093 · doi:10.1007/978-3-319-04921-2_37 |
| [24] | Křetínský, J.; Meggendorfer, T.; Sickert, S.; Lahiri, SK; Wang, C., Owl: a library for \(\omega \)-words, automata, and LTL, Automated Technology for Verification and Analysis, 543-550 (2018), Cham: Springer, Cham · Zbl 1517.68203 · doi:10.1007/978-3-030-01090-4_34 |
| [25] | Kwiatkowska, M.; Norman, G.; Parker, D.; Gopalakrishnan, G.; Qadeer, S., PRISM 4.0: verification of probabilistic real-time systems, Computer Aided Verification, 585-591 (2011), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-642-22110-1_47 |
| [26] | Löding, C., Pirogov, A.: Determinization of Büchi automata: unifying the approaches of Safra and Muller-Schupp. In: International Colloquium on Automata, Languages, and Programming (ICALP). LIPIcs (2019) · Zbl 1437.68101 |
| [27] | Major, J.; Blahoudek, F.; Strejček, J.; Sasaráková, M.; Zbončáková, T.; Chen, Y-F; Cheng, C-H; Esparza, J., ltl3tela: LTL to small deterministic or nondeterministic Emerson-Lei automata, Automated Technology for Verification and Analysis, 357-365 (2019), Cham: Springer, Cham · doi:10.1007/978-3-030-31784-3_21 |
| [28] | Miyano, S.; Hayashi, T., Alternating finite automata on \(\omega \)-words, Theoret. Comput. Sci., 32, 3, 321-330 (1984) · Zbl 0544.68042 · doi:10.1016/0304-3975(84)90049-5 |
| [29] | Müller, D.: Alternative automata-based approaches to probabilistic model checking. Ph.D. thesis, Technische Universität Dresden, November 2019 |
| [30] | Müller, D., Sickert, S.: LTL to deterministic Emerson-Lei automata. In: Games, Automata, Logics and Formal Verification (GandALF). EPTCS (2017) · Zbl 1483.68177 |
| [31] | Muller, DE; Schupp, PE, Simulating alternating tree automata by nondeterministic automata: new results and new proofs of the theorems of Rabin, McNaughton and Safra, Theoret. Comput. Sci., 141, 1, 69-107 (1995) · Zbl 0873.68135 · doi:10.1016/0304-3975(94)00214-4 |
| [32] | Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Symposium on Principles of Programming Languages (POPL). Association for Computing Machinery (ACM), New York, NY, USA (1989) · Zbl 0686.68015 |
| [33] | Redziejowski, RR, An improved construction of deterministic omega-automaton using derivatives, Fund. Inform., 119, 3-4, 393-406 (2012) · Zbl 1279.68173 |
| [34] | Renkin, F.; Duret-Lutz, A.; Pommellet, A.; Hung, DV; Sokolsky, O., Practical “paritizing” of Emerson-Lei automata, Automated Technology for Verification and Analysis, 127-143 (2020), Cham: Springer, Cham · Zbl 1517.68214 · doi:10.1007/978-3-030-59152-6_7 |
| [35] | Safra, S., Vardi, M.Y.: On omega-automata and temporal logic. In: Symposium on Theory of Computing (STOC). Association for Computing Machinery (ACM), New York, NY, USA (1989) |
| [36] | Safra, S.: Complexity of automata on infinite objects. Ph.D. thesis, Weizmann Institute of Science, Rehovot, Israel (1989) |
| [37] | Schewe, S.; Varghese, T.; Chakraborty, S.; Mukund, M., Tight bounds for the determinisation and complementation of generalised Büchi automata, Automated Technology for Verification and Analysis, 42-56 (2012), Heidelberg: Springer, Heidelberg · Zbl 1374.68265 · doi:10.1007/978-3-642-33386-6_5 |
| [38] | Sickert, S.; Esparza, J.; Jaax, S.; Křetínský, J.; Chaudhuri, S.; Farzan, A., Limit-deterministic Büchi automata for linear temporal logic, Computer Aided Verification, 312-332 (2016), Cham: Springer, Cham · Zbl 1411.68054 · doi:10.1007/978-3-319-41540-6_17 |
| [39] | Vardi, M.Y.: Automatic verification of probabilistic concurrent finite state programs. In: Symposium on Foundations of Computer Science (SFCS) (1985) |
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.
