{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T18:00:26Z","timestamp":1781028026651,"version":"3.54.1"},"publisher-location":"Cham","reference-count":55,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031308222","type":"print"},{"value":"9783031308239","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,4,22]],"date-time":"2023-04-22T00:00:00Z","timestamp":1682121600000},"content-version":"vor","delay-in-days":111,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Complementation of nondeterministic B\u00fcchi automata (BAs) is an important problem in automata theory with numerous applications in formal verification, such as termination analysis of programs, model checking, or in decision procedures of some logics. We build on ideas from a\u00a0recent work on BA determinization by Li\n                    <jats:italic>et al.<\/jats:italic>\n                    and propose a\u00a0new modular algorithm for BA complementation. Our algorithm allows to combine several BA complementation procedures together, with one procedure for a\u00a0subset of the BA\u2019s strongly connected components (SCCs). In this way, one can exploit the structure of particular SCCs (such as when they are inherently weak or deterministic) and use more efficient specialized algorithms, regardless of the structure of the whole\u00a0BA. We give a\u00a0general framework into which partial complementation procedures can be plugged in, and its instantiation with several algorithms. The framework can, in general, produce a complement with an Emerson-Lei acceptance condition, which can often be more compact. Using the algorithm, we were able to establish an exponentially better new upper bound of\u00a0\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\mathcal {O}(4^n)$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mrow>\n                            <mml:mi>O<\/mml:mi>\n                            <mml:mo>(<\/mml:mo>\n                            <mml:msup>\n                              <mml:mn>4<\/mml:mn>\n                              <mml:mi>n<\/mml:mi>\n                            <\/mml:msup>\n                            <mml:mo>)<\/mml:mo>\n                          <\/mml:mrow>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    for complementation of the recently introduced class of elevator automata. We implemented the algorithm in a\u00a0prototype and performed a\u00a0comprehensive set of experiments on a\u00a0large set of benchmarks, showing that our framework complements well the state of the art and that it can serve as a\u00a0basis for future efficient BA complementation and inclusion checking algorithms.\n                  <\/jats:p>","DOI":"10.1007\/978-3-031-30823-9_13","type":"book-chapter","created":{"date-parts":[[2023,4,21]],"date-time":"2023-04-21T16:19:12Z","timestamp":1682093952000},"page":"249-270","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Modular Mix-and-Match Complementation of B\u00fcchi Automata"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4375-7954","authenticated-orcid":false,"given":"Vojt\u011bch","family":"Havlena","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3038-5875","authenticated-orcid":false,"given":"Ond\u0159ej","family":"Leng\u00e1l","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7301-9234","authenticated-orcid":false,"given":"Yong","family":"Li","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1184-4669","authenticated-orcid":false,"given":"Barbora","family":"\u0160mahl\u00edkov\u00e1","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4343-9323","authenticated-orcid":false,"given":"Andrea","family":"Turrini","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2023,4,22]]},"reference":[{"key":"13_CR1","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Chen, Y., Hol\u00edk, L., Vojnar, T.: Mediating for reduction (on minimizing alternating b\u00fcchi automata). Theor. Comput. Sci. 552, 26\u201343 (2014). https:\/\/doi.org\/10.1016\/j.tcs.2014.08.003, https:\/\/doi.org\/10.1016\/j.tcs.2014.08.003","DOI":"10.1016\/j.tcs.2014.08.003"},{"key":"13_CR2","doi-asserted-by":"publisher","unstructured":"Allred, J.D., Ultes-Nitsche, U.: A simple and optimal complementation algorithm for B\u00fcchi automata. In: Dawar, A., Gr\u00e4del, E. (eds.) Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018. pp. 46\u201355. ACM (2018). https:\/\/doi.org\/10.1145\/3209108.3209138, https:\/\/doi.org\/10.1145\/3209108.3209138","DOI":"10.1145\/3209108.3209138"},{"key":"13_CR3","doi-asserted-by":"publisher","unstructured":"Beyer, D., L\u00f6we, S., Wendler, P.: Reliable benchmarking: requirements and solutions. Int. J. Softw. Tools Technol. Transf. 21(1), 1\u201329 (2019). https:\/\/doi.org\/10.1007\/s10009-017-0469-y, https:\/\/doi.org\/10.1007\/s10009-017-0469-y","DOI":"10.1007\/s10009-017-0469-y"},{"key":"13_CR4","doi-asserted-by":"publisher","unstructured":"Blahoudek, F., Duret-Lutz, A., Klokocka, M., Kret\u00ednsk\u00fd, M., Strejcek, J.: Seminator: A tool for semi-determinization of omega-automata. In: Eiter, T., Sands, D. (eds.) LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017. EPiC Series in Computing, vol.\u00a046, pp. 356\u2013367. EasyChair (2017). https:\/\/doi.org\/10.29007\/k5nl, https:\/\/doi.org\/10.29007\/k5nl","DOI":"10.29007\/k5nl"},{"key":"13_CR5","doi-asserted-by":"publisher","unstructured":"Blahoudek, F., Duret-Lutz, A., Strejcek, J.: Seminator\u00a02 can complement generalized B\u00fcchi automata via improved semi-determinization. In: Lahiri, S.K., Wang, C. (eds.) Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II. Lecture Notes in Computer Science, vol. 12225, pp. 15\u201327. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_2, https:\/\/doi.org\/10.1007\/978-3-030-53291-8_2","DOI":"10.1007\/978-3-030-53291-8_2"},{"key":"13_CR6","doi-asserted-by":"publisher","unstructured":"Blahoudek, F., Heizmann, M., Schewe, S., Strej\u010dek, J., Tsai, M.: Complementing semi-deterministic B\u00fcchi automata. In: Chechik, M., Raskin, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings. Lecture Notes in Computer Science, vol.\u00a09636, pp. 770\u2013787. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_49, https:\/\/doi.org\/10.1007\/978-3-662-49674-9_49","DOI":"10.1007\/978-3-662-49674-9_49"},{"key":"13_CR7","doi-asserted-by":"publisher","unstructured":"Breuers, S., L\u00f6ding, C., Olschewski, J.: Improved Ramsey-based B\u00fcchi complementation. In: Birkedal, L. (ed.) Foundations of Software Science and Computational Structures - 15th International Conference, FOSSACS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings. Lecture Notes in Computer Science, vol.\u00a07213, pp. 150\u2013164. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-28729-9_10, https:\/\/doi.org\/10.1007\/978-3-642-28729-9_10","DOI":"10.1007\/978-3-642-28729-9_10"},{"key":"13_CR8","doi-asserted-by":"publisher","unstructured":"B\u00fcchi, J.R.: On a decision method in restricted second order arithmetic. In: Mac\u00a0Lane, S., Siefkes, D. (eds.) The Collected Works of J. Richard B\u00fcchi, pp. 425\u2013435. Springer (1990). https:\/\/doi.org\/10.1007\/978-1-4613-8928-6_23, https:\/\/doi.org\/10.1007\/978-1-4613-8928-6_23","DOI":"10.1007\/978-1-4613-8928-6_23"},{"key":"13_CR9","doi-asserted-by":"crossref","unstructured":"Bustan, D., Grumberg, O.: Simulation-based Minimization. ACM Transactions on Computational Logic 4(2), 181\u2013206 (2003)","DOI":"10.1145\/635499.635502"},{"key":"13_CR10","doi-asserted-by":"publisher","unstructured":"Chen, Y., Havlena, V., Leng\u00e1l, O.: Simulations in rank-based B\u00fcchi automata complementation. In: Lin, A.W. (ed.) Programming Languages and Systems - 17th Asian Symposium, APLAS 2019, Nusa Dua, Bali, Indonesia, December 1-4, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11893, pp. 447\u2013467. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-34175-6_23, https:\/\/doi.org\/10.1007\/978-3-030-34175-6_23","DOI":"10.1007\/978-3-030-34175-6_23"},{"key":"13_CR11","doi-asserted-by":"publisher","unstructured":"Chen, Y., Heizmann, M., Leng\u00e1l, O., Li, Y., Tsai, M., Turrini, A., Zhang, L.: Advanced automata-based algorithms for program termination checking. In: Foster, J.S., Grossman, D. (eds.) Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, Philadelphia, PA, USA, June 18-22, 2018. pp. 135\u2013150. ACM (2018). https:\/\/doi.org\/10.1145\/3192366.3192405, https:\/\/doi.org\/10.1145\/3192366.3192405","DOI":"10.1145\/3192366.3192405"},{"key":"13_CR12","doi-asserted-by":"publisher","unstructured":"Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N., S\u00e1nchez, C.: Temporal logics for hyperproperties. In: Abadi, M., Kremer, S. (eds.) Principles of Security and Trust - Third International Conference, POST 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings. Lecture Notes in Computer Science, vol.\u00a08414, pp. 265\u2013284. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-642-54792-8_15, https:\/\/doi.org\/10.1007\/978-3-642-54792-8_15","DOI":"10.1007\/978-3-642-54792-8_15"},{"key":"13_CR13","doi-asserted-by":"publisher","unstructured":"Clemente, L., Mayr, R.: Efficient reduction of nondeterministic automata with application to language inclusion testing. Log. Methods Comput. Sci. 15(1) (2019). https:\/\/doi.org\/10.23638\/LMCS-15(1:12)2019, https:\/\/doi.org\/10.23638\/LMCS-15(1:12)2019","DOI":"10.23638\/LMCS-15(1:12)2019"},{"key":"13_CR14","doi-asserted-by":"publisher","unstructured":"Courcoubetis, C., Yannakakis, M.: Verifying temporal properties of finite-state probabilistic programs. In: 29th Annual Symposium on Foundations of Computer Science, White Plains, New York, USA, 24-26 October 1988. pp. 338\u2013345. IEEE Computer Society (1988). https:\/\/doi.org\/10.1109\/SFCS.1988.21950, https:\/\/doi.org\/10.1109\/SFCS.1988.21950","DOI":"10.1109\/SFCS.1988.21950"},{"key":"13_CR15","doi-asserted-by":"crossref","unstructured":"Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, E., Xu, L.: Spot\u00a02.0 - A framework for LTL and $$\\omega $$-automata manipulation. In: Artho, C., Legay, A., Peled, D. (eds.) Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings. Lecture Notes in Computer Science, vol.\u00a09938, pp. 122\u2013129 (2016). 10.1007\/978-3-319-46520-3_8, https:\/\/doi.org\/10.1007\/978-3-319-46520-3_8","DOI":"10.1007\/978-3-319-46520-3_8"},{"key":"13_CR16","doi-asserted-by":"publisher","unstructured":"Duret-Lutz, A., Renault, E., Colange, M., Renkin, F., Aisse, A.G., Schlehuber-Caissier, P., Medioni, T., Martin, A., Dubois, J., Gillard, C., Lauko, H.: From Spot\u00a02.0 to Spot\u00a02.10: What\u2019s new? In: Shoham, S., Vizel, Y. (eds.) Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part II. Lecture Notes in Computer Science, vol. 13372, pp. 174\u2013187. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-13188-2_9, https:\/\/doi.org\/10.1007\/978-3-031-13188-2_9","DOI":"10.1007\/978-3-031-13188-2_9"},{"key":"13_CR17","doi-asserted-by":"publisher","unstructured":"Esparza, J., Kret\u00ednsk\u00fd, J., Raskin, J., Sickert, S.: From LTL and limit-deterministic B\u00fcchi automata to deterministic parity automata. In: Legay, A., Margaria, T. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part I. Lecture Notes in Computer Science, vol. 10205, pp. 426\u2013442 (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_25, https:\/\/doi.org\/10.1007\/978-3-662-54577-5_25","DOI":"10.1007\/978-3-662-54577-5_25"},{"key":"13_CR18","doi-asserted-by":"publisher","unstructured":"Etessami, K., Wilke, T., Schuller, R.A.: Fair simulation relations, parity games, and state space reduction for B\u00fcchi automata. SIAM J. Comput. 34(5), 1159\u20131175 (2005). https:\/\/doi.org\/10.1137\/S0097539703420675, https:\/\/doi.org\/10.1137\/S0097539703420675","DOI":"10.1137\/S0097539703420675"},{"key":"13_CR19","doi-asserted-by":"publisher","unstructured":"Fogarty, S., Kupferman, O., Vardi, M.Y., Wilke, T.: Profile trees for B\u00fcchi word automata, with application to determinization. Inf. Comput. 245, 136\u2013151 (2015). https:\/\/doi.org\/10.1016\/j.ic.2014.12.021, https:\/\/doi.org\/10.1016\/j.ic.2014.12.021","DOI":"10.1016\/j.ic.2014.12.021"},{"key":"13_CR20","doi-asserted-by":"publisher","unstructured":"Fogarty, S., Kupferman, O., Wilke, T., Vardi, M.Y.: Unifying B\u00fcchi complementation constructions. Log. Methods Comput. Sci. 9(1) (2013). https:\/\/doi.org\/10.2168\/LMCS-9(1:13)2013, https:\/\/doi.org\/10.2168\/LMCS-9(1:13)2013","DOI":"10.2168\/LMCS-9(1:13)2013"},{"key":"13_CR21","doi-asserted-by":"publisher","unstructured":"Friedgut, E., Kupferman, O., Vardi, M.Y.: B\u00fcchi complementation made tighter. Int. J. Found. Comput. Sci. 17(4), 851\u2013868 (2006). https:\/\/doi.org\/10.1142\/S0129054106004145, https:\/\/doi.org\/10.1142\/S0129054106004145","DOI":"10.1142\/S0129054106004145"},{"key":"13_CR22","doi-asserted-by":"publisher","unstructured":"Gurumurthy, S., Kupferman, O., Somenzi, F., Vardi, M.Y.: On complementing nondeterministic B\u00fcchi automata. In: Geist, D., Tronci, E. (eds.) Correct Hardware Design and Verification Methods, 12th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2003, L\u2019Aquila, Italy, October 21-24, 2003, Proceedings. Lecture Notes in Computer Science, vol.\u00a02860, pp. 96\u2013110. Springer (2003). https:\/\/doi.org\/10.1007\/978-3-540-39724-3_10, https:\/\/doi.org\/10.1007\/978-3-540-39724-3_10","DOI":"10.1007\/978-3-540-39724-3_10"},{"key":"13_CR23","doi-asserted-by":"publisher","unstructured":"Havlena, V., Leng\u00e1l, O., Smahl\u00edkov\u00e1, B.: Deciding S1S: down the rabbit hole and through the looking glass. In: Echihabi, K., Meyer, R. (eds.) Networked Systems - 9th International Conference, NETYS 2021, Virtual Event, May 19-21, 2021, Proceedings. Lecture Notes in Computer Science, vol. 12754, pp. 215\u2013222. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-91014-3_15, https:\/\/doi.org\/10.1007\/978-3-030-91014-3_15","DOI":"10.1007\/978-3-030-91014-3_15"},{"key":"13_CR24","doi-asserted-by":"publisher","unstructured":"Havlena, V., Leng\u00e1l, O.: Reducing (to) the ranks: Efficient rank-based B\u00fcchi automata complementation. In: Haddad, S., Varacca, D. (eds.) 32nd International Conference on Concurrency Theory, CONCUR 2021, August 24-27, 2021, Virtual Conference. LIPIcs, vol.\u00a0203, pp. 2:1\u20132:19. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2021.2, https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2021.2","DOI":"10.4230\/LIPIcs.CONCUR.2021.2"},{"key":"13_CR25","unstructured":"Havlena, V., Leng\u00e1l, O., Li, Y., \u0160mahl\u00edkov\u00e1, B., Turrini, A.: Kofola (2022), https:\/\/github.com\/VeriFIT\/kofola"},{"key":"13_CR26","doi-asserted-by":"publisher","unstructured":"Havlena, V., Leng\u00e1l, O., Li, Y., \u0160mahl\u00edkov\u00e1, B., Turrini, A.: Artifact for the TACAS\u201923 paper \u201cModular Mix-and-Match Complementation of B\u00fcchi Automata\u201d (Jan 2023). https:\/\/doi.org\/10.5281\/zenodo.7505210, https:\/\/doi.org\/10.5281\/zenodo.7505210","DOI":"10.5281\/zenodo.7505210"},{"key":"13_CR27","doi-asserted-by":"publisher","unstructured":"Havlena, V., Leng\u00e1l, O., Li, Y., \u0160mahl\u00edkov\u00e1, B., Turrini, A.: Modular mix-and-match complementation of B\u00fcchi automata (technical report). CoRR abs\/2301.01890 (2023). https:\/\/doi.org\/10.48550\/arXiv.2301.01890, https:\/\/doi.org\/10.48550\/arXiv.2301.01890","DOI":"10.48550\/arXiv.2301.01890"},{"key":"13_CR28","doi-asserted-by":"publisher","unstructured":"Havlena, V., Leng\u00e1l, O., \u0160mahl\u00edkov\u00e1, B.: Complementing B\u00fcchi automata with Ranker. In: Shoham, S., Vizel, Y. (eds.) Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part II. Lecture Notes in Computer Science, vol. 13372, pp. 188\u2013201. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-13188-2_10, https:\/\/doi.org\/10.1007\/978-3-031-13188-2_10","DOI":"10.1007\/978-3-031-13188-2_10"},{"key":"13_CR29","doi-asserted-by":"publisher","unstructured":"Havlena, V., Leng\u00e1l, O., \u0160mahl\u00edkov\u00e1, B.: Sky is not the limit: Tighter rank bounds for elevator automata in B\u00fcchi automata complementation. In: Fisman, D., Rosu, G. (eds.) 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. Lecture Notes in Computer Science, vol. 13244, pp. 118\u2013136. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_7, https:\/\/doi.org\/10.1007\/978-3-030-99527-0_7","DOI":"10.1007\/978-3-030-99527-0_7"},{"key":"13_CR30","doi-asserted-by":"publisher","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Termination analysis by learning terminating programs. In: Biere, A., Bloem, R. (eds.) Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings. Lecture Notes in Computer Science, vol.\u00a08559, pp. 797\u2013813. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_53, https:\/\/doi.org\/10.1007\/978-3-319-08867-9_53","DOI":"10.1007\/978-3-319-08867-9_53"},{"key":"13_CR31","doi-asserted-by":"publisher","unstructured":"Hieronymi, P., Ma, D., Oei, R., Schaeffer, L., Schulz, C., Shallit, J.O.: Decidability for Sturmian words. In: Manea, F., Simpson, A. (eds.) 30th EACSL Annual Conference on Computer Science Logic, CSL 2022, February 14-19, 2022, G\u00f6ttingen, Germany (Virtual Conference). LIPIcs, vol.\u00a0216, pp. 24:1\u201324:23. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022). https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2022.24, https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2022.24","DOI":"10.4230\/LIPIcs.CSL.2022.24"},{"key":"13_CR32","doi-asserted-by":"publisher","unstructured":"K\u00e4hler, D., Wilke, T.: Complementation, disambiguation, and determinization of B\u00fcchi automata unified. In: Aceto, L., Damg\u00e5rd, I., Goldberg, L.A., Halld\u00f3rsson, M.M., Ing\u00f3lfsd\u00f3ttir, A., Walukiewicz, I. (eds.) 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. Lecture Notes in Computer Science, vol.\u00a05125, pp. 724\u2013735. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-70575-8_59, https:\/\/doi.org\/10.1007\/978-3-540-70575-8_59","DOI":"10.1007\/978-3-540-70575-8_59"},{"key":"13_CR33","doi-asserted-by":"publisher","unstructured":"Karmarkar, H., Chakraborty, S.: On minimal odd rankings for B\u00fcchi complementation. In: Liu, Z., Ravn, A.P. (eds.) Automated Technology for Verification and Analysis, 7th International Symposium, ATVA 2009, Macao, China, October 14-16, 2009. Proceedings. Lecture Notes in Computer Science, vol.\u00a05799, pp. 228\u2013243. Springer (2009). https:\/\/doi.org\/10.1007\/978-3-642-04761-9_18, https:\/\/doi.org\/10.1007\/978-3-642-04761-9_18","DOI":"10.1007\/978-3-642-04761-9_18"},{"key":"13_CR34","doi-asserted-by":"publisher","unstructured":"Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. ACM Trans. Comput. Log. 2(3), 408\u2013429 (2001). https:\/\/doi.org\/10.1145\/377978.377993, https:\/\/doi.org\/10.1145\/377978.377993","DOI":"10.1145\/377978.377993"},{"key":"13_CR35","doi-asserted-by":"publisher","unstructured":"Kurshan, R.P.: Complementing deterministic B\u00fcchi automata in polynomial time. J. Comput. Syst. Sci. 35(1), 59\u201371 (1987). https:\/\/doi.org\/10.1016\/0022-0000(87)90036-5, https:\/\/doi.org\/10.1016\/0022-0000(87)90036-5","DOI":"10.1016\/0022-0000(87)90036-5"},{"key":"13_CR36","unstructured":"Leng\u00e1l, O.: Automata benchmarks (2022), https:\/\/github.com\/ondrik\/automata-benchmarks"},{"key":"13_CR37","doi-asserted-by":"publisher","unstructured":"Li, Y., Turrini, A., Feng, W., Vardi, M.Y., Zhang, L.: Divide-and-conquer determinization of B\u00fcchi automata based on SCC decomposition. In: Shoham, S., Vizel, Y. (eds.) Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part II. Lecture Notes in Computer Science, vol. 13372, pp. 152\u2013173. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-13188-2_8, https:\/\/doi.org\/10.1007\/978-3-031-13188-2_8","DOI":"10.1007\/978-3-031-13188-2_8"},{"key":"13_CR38","doi-asserted-by":"publisher","unstructured":"Li, Y., Turrini, A., Zhang, L., Schewe, S.: Learning to complement B\u00fcchi automata. In: Dillig, I., Palsberg, J. (eds.) Verification, Model Checking, and Abstract Interpretation - 19th International Conference, VMCAI 2018, Los Angeles, CA, USA, January 7-9, 2018, Proceedings. Lecture Notes in Computer Science, vol. 10747, pp. 313\u2013335. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-73721-8_15, https:\/\/doi.org\/10.1007\/978-3-319-73721-8_15","DOI":"10.1007\/978-3-319-73721-8_15"},{"key":"13_CR39","doi-asserted-by":"publisher","unstructured":"Li, Y., Vardi, M.Y., Zhang, L.: On the power of unambiguity in B\u00fcchi complementation. In: Raskin, J., Bresolin, D. (eds.) Proceedings 11th International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2020, Brussels, Belgium, September 21-22, 2020. EPTCS, vol.\u00a0326, pp. 182\u2013198 (2020). https:\/\/doi.org\/10.4204\/EPTCS.326.12, https:\/\/doi.org\/10.4204\/EPTCS.326.12","DOI":"10.4204\/EPTCS.326.12"},{"key":"13_CR40","doi-asserted-by":"publisher","unstructured":"L\u00f6ding, C.: Optimal bounds for transformations of omega-automata. In: Rangan, C.P., Raman, V., Ramanujam, R. (eds.) Foundations of Software Technology and Theoretical Computer Science, 19th Conference, Chennai, India, December 13-15, 1999, Proceedings. Lecture Notes in Computer Science, vol.\u00a01738, pp. 97\u2013109. Springer (1999). https:\/\/doi.org\/10.1007\/3-540-46691-6_8, https:\/\/doi.org\/10.1007\/3-540-46691-6_8","DOI":"10.1007\/3-540-46691-6_8"},{"key":"13_CR41","doi-asserted-by":"publisher","unstructured":"L\u00f6ding, C., Pirogov, A.: New optimizations and heuristics for determinization of B\u00fcchi automata. In: Chen, Y., Cheng, C., Esparza, J. (eds.) Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11781, pp. 317\u2013333. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-31784-3_18, https:\/\/doi.org\/10.1007\/978-3-030-31784-3_18","DOI":"10.1007\/978-3-030-31784-3_18"},{"key":"13_CR42","doi-asserted-by":"publisher","unstructured":"Miyano, S., Hayashi, T.: Alternating finite automata on omega-words. Theor. Comput. Sci. 32, 321\u2013330 (1984). https:\/\/doi.org\/10.1016\/0304-3975(84)90049-5, https:\/\/doi.org\/10.1016\/0304-3975(84)90049-5","DOI":"10.1016\/0304-3975(84)90049-5"},{"key":"13_CR43","doi-asserted-by":"publisher","unstructured":"Piterman, N.: From nondeterministic B\u00fcchi and Streett automata to deterministic parity automata. Log. Methods Comput. Sci. 3(3) (2007). https:\/\/doi.org\/10.2168\/LMCS-3(3:5)2007, https:\/\/doi.org\/10.2168\/LMCS-3(3:5)2007","DOI":"10.2168\/LMCS-3(3:5)2007"},{"key":"13_CR44","doi-asserted-by":"publisher","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1 November 1977. pp. 46\u201357. IEEE Computer Society (1977). https:\/\/doi.org\/10.1109\/SFCS.1977.32, https:\/\/doi.org\/10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"key":"13_CR45","doi-asserted-by":"publisher","unstructured":"Redziejowski, R.R.: An improved construction of deterministic omega-automaton using derivatives. Fundam. Informaticae 119(3-4), 393\u2013406 (2012). https:\/\/doi.org\/10.3233\/FI-2012-744, https:\/\/doi.org\/10.3233\/FI-2012-744","DOI":"10.3233\/FI-2012-744"},{"key":"13_CR46","doi-asserted-by":"publisher","unstructured":"Safra, S.: On the complexity of omega-automata. In: 29th Annual Symposium on Foundations of Computer Science, White Plains, New York, USA, 24-26 October 1988. pp. 319\u2013327. IEEE Computer Society (1988). https:\/\/doi.org\/10.1109\/SFCS.1988.21948, https:\/\/doi.org\/10.1109\/SFCS.1988.21948","DOI":"10.1109\/SFCS.1988.21948"},{"key":"13_CR47","doi-asserted-by":"publisher","unstructured":"Safra, S., Vardi, M.Y.: On omega-automata and temporal logic (preliminary report). In: Johnson, D.S. (ed.) Proceedings of the 21st Annual ACM Symposium on Theory of Computing, May 14-17, 1989, Seattle, Washington, USA. pp. 127\u2013137. ACM (1989). https:\/\/doi.org\/10.1145\/73007.73019, https:\/\/doi.org\/10.1145\/73007.73019","DOI":"10.1145\/73007.73019"},{"key":"13_CR48","doi-asserted-by":"publisher","unstructured":"Schewe, S.: B\u00fcchi complementation made tight. In: Albers, S., Marion, J. (eds.) 26th International Symposium on Theoretical Aspects of Computer Science, STACS 2009, February 26-28, 2009, Freiburg, Germany, Proceedings. LIPIcs, vol.\u00a03, pp. 661\u2013672. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, Germany (2009). https:\/\/doi.org\/10.4230\/LIPIcs.STACS.2009.1854, https:\/\/doi.org\/10.4230\/LIPIcs.STACS.2009.1854","DOI":"10.4230\/LIPIcs.STACS.2009.1854"},{"key":"13_CR49","doi-asserted-by":"publisher","unstructured":"Sickert, S., Esparza, J., Jaax, S., Kret\u00ednsk\u00fd, J.: Limit-deterministic B\u00fcchi automata for linear temporal logic. In: Chaudhuri, S., Farzan, A. (eds.) Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II. Lecture Notes in Computer Science, vol.\u00a09780, pp. 312\u2013332. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_17, https:\/\/doi.org\/10.1007\/978-3-319-41540-6_17","DOI":"10.1007\/978-3-319-41540-6_17"},{"key":"13_CR50","doi-asserted-by":"publisher","unstructured":"Sistla, A.P., Vardi, M.Y., Wolper, P.: The complementation problem for B\u00fcchi automata with applications to temporal logic. Theor. Comput. Sci. 49, 217\u2013237 (1987). https:\/\/doi.org\/10.1016\/0304-3975(87)90008-9, https:\/\/doi.org\/10.1016\/0304-3975(87)90008-9","DOI":"10.1016\/0304-3975(87)90008-9"},{"key":"13_CR51","unstructured":"The SV-COMP Community: International competition on software verification (2022), https:\/\/sv-comp.sosy-lab.org\/"},{"key":"13_CR52","doi-asserted-by":"publisher","unstructured":"Tsai, M., Fogarty, S., Vardi, M.Y., Tsay, Y.: State of B\u00fcchi complementation. Log. Methods Comput. Sci. 10(4) (2014). https:\/\/doi.org\/10.2168\/LMCS-10(4:13)2014, https:\/\/doi.org\/10.2168\/LMCS-10(4:13)2014","DOI":"10.2168\/LMCS-10(4:13)2014"},{"key":"13_CR53","unstructured":"Vardi, M.Y., Wilke, T.: Automata: from logics to algorithms. In: Flum, J., Gr\u00e4del, E., Wilke, T. (eds.) Logic and Automata: History and Perspectives. Texts in Logic and Games, vol.\u00a02, pp. 629\u2013736. Amsterdam University Press (2008)"},{"key":"13_CR54","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification (preliminary report). In: Proceedings of the Symposium on Logic in Computer Science (LICS \u201986), Cambridge, Massachusetts, USA, June 16-18, 1986. pp. 332\u2013344. IEEE Computer Society (1986)"},{"key":"13_CR55","doi-asserted-by":"publisher","unstructured":"Yan, Q.: Lower bounds for complementation of omega-automata via the full automata technique. Log. Methods Comput. Sci. 4(1) (2008). https:\/\/doi.org\/10.2168\/LMCS-4(1:5)2008, https:\/\/doi.org\/10.2168\/LMCS-4(1:5)2008","DOI":"10.2168\/LMCS-4(1:5)2008"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-30823-9_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T17:05:16Z","timestamp":1781024716000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-30823-9_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031308222","9783031308239"],"references-count":55,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-30823-9_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"22 April 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 April 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2023\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}