{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,23]],"date-time":"2025-09-23T12:34:11Z","timestamp":1758630851808,"version":"3.40.4"},"publisher-location":"Cham","reference-count":45,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031908965"},{"type":"electronic","value":"9783031908972"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>We give new constructions for complementing subclasses\u00a0of Emerson-Lei automata using modifications of rank-based B\u00fcchi automata complementation. In particular, we propose a\u00a0specialized rank-based construction for a\u00a0Boolean combination of Inf acceptance conditions, which heavily relies on a\u00a0novel\u00a0way of a\u00a0run DAG labelling enhancing the ranking functions with models of\u00a0the acceptance condition. Moreover, we propose a technique for complementing generalized Rabin automata, which are structurally as concise as general Emerson-Lei automata (but can have a larger acceptance condition). The construction is modular in the sense that it extends a given complementation algorithm for a condition\u00a0<jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$\\varphi $$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>\u03c6<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula> in a way that the resulting procedure handles conditions of the form\u00a0<jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$\\text {Fin}\\wedge \\varphi $$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mtext>Fin<\/mml:mtext>\n                    <mml:mo>\u2227<\/mml:mo>\n                    <mml:mi>\u03c6<\/mml:mi>\n                  <\/mml:mrow>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>. The proposed constructions give upper bounds that are exponentially better\u00a0than the state of the art for some of the classes.<\/jats:p>","DOI":"10.1007\/978-3-031-90897-2_5","type":"book-chapter","created":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T08:18:11Z","timestamp":1746001091000},"page":"88-110","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Complementation of Emerson-Lei 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":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3038-5875","authenticated-orcid":false,"given":"Ond\u0159ej","family":"Leng\u00e1l","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1184-4669","authenticated-orcid":false,"given":"Barbora","family":"\u0160mahl\u00edkov\u00e1","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"key":"5_CR1","doi-asserted-by":"publisher","unstructured":"Jo\u00ebl\u00a0D. Allred and Ulrich Ultes-Nitsche. A simple and optimal complementation algorithm for B\u00fcchi automata. In Anuj Dawar and Erich Gr\u00e4del, editors, Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 46\u201355. ACM, 2018. https:\/\/doi.org\/10.1145\/3209108.3209138.","DOI":"10.1145\/3209108.3209138"},{"key":"5_CR2","doi-asserted-by":"publisher","unstructured":"Frantisek Blahoudek, Matthias Heizmann, Sven Schewe, Jan Strejcek, and Ming-Hsien Tsai. Complementing semi-deterministic B\u00fcchi automata. In Marsha Chechik and Jean-Fran\u00e7ois Raskin, editors, 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, volume 9636 of Lecture Notes in Computer Science, pages 770\u2013787. Springer, 2016. https:\/\/doi.org\/10.1007\/978-3-662-49674-9_49.","DOI":"10.1007\/978-3-662-49674-9_49"},{"key":"5_CR3","doi-asserted-by":"publisher","unstructured":"Franti\u0161ek Blahoudek, Alexandre Duret-Lutz, and Jan Strej\u010dek. Seminator\u00a02 can complement generalized B\u00fcchi automata via improved semi-determinization. In Proceedings of the 32nd International Conference on Computer-Aided Verification (CAV\u201920), volume 12225 of Lecture Notes in Computer Science, pages 15\u201327. Springer, July 2020. https:\/\/doi.org\/10.1007\/978-3-030-53291-8_2.","DOI":"10.1007\/978-3-030-53291-8_2"},{"key":"5_CR4","unstructured":"Udi Boker. Why these automata types? In LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Awassa, Ethiopia, 16-21 November 2018, volume\u00a057 of EPiC Series in Computing, pages 143\u2013163. EasyChair, 2018."},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"Stefan Breuers, Christof L\u00f6ding, and J\u00f6rg Olschewski. Improved Ramsey-based B\u00fcchi complementation. In Proc. of FOSSACS\u201912, pages 150\u2013164. Springer, 2012.","DOI":"10.1007\/978-3-642-28729-9_10"},{"key":"5_CR6","unstructured":"J.\u00a0Richard B\u00fcchi. On a decision method in restricted second order arithmetic. In Proc. of International Congress on Logic, Method, and Philosophy of Science 1960. Stanford Univ. Press, Stanford, 1962."},{"key":"5_CR7","doi-asserted-by":"publisher","unstructured":"Yang Cai and Ting Zhang. Tight upper bounds for Streett and parity complementation. In Marc Bezem, editor, Computer Science Logic, 25th International Workshop \/ 20th Annual Conference of the EACSL, CSL 2011, September 12-15, 2011, Bergen, Norway, Proceedings, volume\u00a012 of LIPIcs, pages 112\u2013128. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 2011. https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2011.112.","DOI":"10.4230\/LIPIcs.CSL.2011.112"},{"key":"5_CR8","doi-asserted-by":"publisher","unstructured":"Yang Cai, Ting Zhang, and Haifeng Luo. An improved lower bound for the complementation of Rabin automata. In Proceedings of the 2009 24th Annual IEEE Symposium on Logic In Computer Science, LICS \u201909, page 167-176, USA, 2009. IEEE Computer Society. https:\/\/doi.org\/10.1109\/LICS.2009.13.","DOI":"10.1109\/LICS.2009.13"},{"key":"5_CR9","doi-asserted-by":"publisher","unstructured":"Yu-Fang Chen, Vojtech Havlena, and Ondrej Leng\u00e1l. Simulations in rank-based B\u00fcchi automata complementation. In Anthony\u00a0Widjaja Lin, editor, Programming Languages and Systems - 17th Asian Symposium, APLAS 2019, Nusa Dua, Bali, Indonesia, December 1-4, 2019, Proceedings, volume 11893 of Lecture Notes in Computer Science, pages 447\u2013467. Springer, 2019. https:\/\/doi.org\/10.1007\/978-3-030-34175-6_23.","DOI":"10.1007\/978-3-030-34175-6_23"},{"key":"5_CR10","doi-asserted-by":"publisher","unstructured":"Michael\u00a0R. Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher\u00a0K. Micinski, Markus\u00a0N. Rabe, and C\u00e9sar S\u00e1nchez. Temporal logics for hyperproperties. In Mart\u00edn Abadi and Steve Kremer, editors, 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, volume 8414 of Lecture Notes in Computer Science, pages 265\u2013284. Springer, 2014. https:\/\/doi.org\/10.1007\/978-3-642-54792-8_15.","DOI":"10.1007\/978-3-642-54792-8_15"},{"key":"5_CR11","doi-asserted-by":"publisher","unstructured":"E.\u00a0Allen Emerson and Chin-Laung Lei. Modalities for model checking: Branching time logic strikes back. Sci. Comput. Program., 8(3):275\u2013306, 1987. https:\/\/doi.org\/10.1016\/0167-6423(87)90036-0.","DOI":"10.1016\/0167-6423(87)90036-0"},{"key":"5_CR12","doi-asserted-by":"publisher","unstructured":"Weizhi Feng, Yong Li, Andrea Turrini, Moshe\u00a0Y. Vardi, and Lijun Zhang. On the power of finite ambiguity in B\u00fcchi complementation. Inf. Comput., 292:105032, 2023. URL: https:\/\/doi.org\/10.1016\/j.ic.2023.105032, https:\/\/doi.org\/10.1016\/J.IC.2023.105032.","DOI":"10.1016\/J.IC.2023.105032"},{"key":"5_CR13","doi-asserted-by":"publisher","unstructured":"Dana Fisman and Yoad Lustig. A modular approach for B\u00fcchi determinization. In Luca Aceto and David de\u00a0Frutos-Escrig, editors, 26th International Conference on Concurrency Theory, CONCUR 2015, Madrid, Spain, September 1.4, 2015, volume\u00a042 of LIPIcs, pages 368\u2013382. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 2015. URL: https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2015.368, https:\/\/doi.org\/10.4230\/LIPICS.CONCUR.2015.368.","DOI":"10.4230\/LIPICS.CONCUR.2015.368"},{"key":"5_CR14","doi-asserted-by":"publisher","unstructured":"Ehud Friedgut, Orna Kupferman, and Moshe\u00a0Y. Vardi. B\u00fcchi complementation made tighter. Int. J. Found. Comput. Sci., 17(4):851\u2013868, 2006. https:\/\/doi.org\/10.1142\/S0129054106004145.","DOI":"10.1142\/S0129054106004145"},{"key":"5_CR15","doi-asserted-by":"publisher","unstructured":"Erich Gr\u00e4del, Wolfgang Thomas, and Thomas Wilke, editors. Automata, Logics, and Infinite Games: A Guide to Current Research [outcome of a Dagstuhl seminar, February 2001], volume 2500 of Lecture Notes in Computer Science. Springer, 2002. https:\/\/doi.org\/10.1007\/3-540-36387-4.","DOI":"10.1007\/3-540-36387-4"},{"key":"5_CR16","doi-asserted-by":"publisher","unstructured":"Vojtech Havlena and Ondrej Leng\u00e1l. Reducing (to) the ranks: Efficient rank-based B\u00fcchi automata complementation. In Serge Haddad and Daniele Varacca, editors, 32nd International Conference on Concurrency Theory, CONCUR 2021, August 24-27, 2021, Virtual Conference, volume 203 of LIPIcs, pages 2:1\u20132:19. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 2021. URL: 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":"5_CR17","doi-asserted-by":"crossref","unstructured":"Vojt\u011bch Havlena, Ond\u0159ej Leng\u00e1l, Yong Li, Barbora \u0160mahl\u00edkov\u00e1, and Andrea Turrini. Modular mix-and-match complementation of B\u00fcchi automata. In Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, Lecture Notes in Computer Science. Springer, 2023.","DOI":"10.1007\/978-3-031-30823-9_13"},{"key":"5_CR18","doi-asserted-by":"publisher","unstructured":"Vojt\u011bch Havlena, Ond\u0159ej Leng\u00e1l, and Barbora \u0160mahl\u00edkov\u00e1. Complementing B\u00fcchi automata with ranker. In Sharon Shoham and Yakir Vizel, editors, Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part II, volume 13372 of Lecture Notes in Computer Science, pages 188\u2013201. Springer, 2022. https:\/\/doi.org\/10.1007\/978-3-031-13188-2_10.","DOI":"10.1007\/978-3-031-13188-2_10"},{"key":"5_CR19","doi-asserted-by":"publisher","unstructured":"Vojt\u011bch Havlena, Ond\u0159ej Leng\u00e1l, and Barbora \u0160mahl\u00edkov\u00e1. Sky is not the limit: Tighter rank bounds for elevator automata in B\u00fcchi automata complementation. 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 118\u2013136. Springer, 2022. https:\/\/doi.org\/10.1007\/978-3-030-99527-0_7.","DOI":"10.1007\/978-3-030-99527-0_7"},{"key":"5_CR20","unstructured":"Vojt\u011bch Havlena, Ond\u0159ej Leng\u00e1l, and Barbora \u0160mahl\u00edkov\u00e1. Complementation of Emerson-Lei automata (technical report). CoRR, abs\/2410.11644, 2024. URL: https:\/\/arxiv.org\/abs\/2410.11644, arXiv:2410.11644."},{"key":"5_CR21","doi-asserted-by":"publisher","unstructured":"Philipp Hieronymi, Dun Ma, Reed Oei, Luke Schaeffer, Christian Schulz, and Jeffrey\u00a0O. Shallit. Decidability for Sturmian words. Log. Methods Comput. Sci., 20(3), 2024. URL: https:\/\/doi.org\/10.46298\/lmcs-20(3:12)2024, https:\/\/doi.org\/10.46298\/LMCS-20(3:12)2024.","DOI":"10.46298\/LMCS-20(3:12)2024"},{"key":"5_CR22","doi-asserted-by":"publisher","unstructured":"Tobias John, Simon Jantsch, Christel Baier, and Sascha Kl\u00fcppelholz. From Emerson-Lei automata to deterministic, limit-deterministic or good-for-MDP automata. Innov. Syst. Softw. Eng., 18(3):385\u2013403, 2022. https:\/\/doi.org\/10.1007\/s11334-022-00445-7.","DOI":"10.1007\/s11334-022-00445-7"},{"key":"5_CR23","doi-asserted-by":"crossref","unstructured":"Detlef K\u00e4hler and Thomas Wilke. Complementation, disambiguation, and determinization of B\u00fcchi automata unified. In Proc. of ICALP\u201908, pages 724\u2013735. Springer, 2008.","DOI":"10.1007\/978-3-540-70575-8_59"},{"key":"5_CR24","doi-asserted-by":"publisher","unstructured":"Hrishikesh Karmarkar and Supratik Chakraborty. On minimal odd rankings for B\u00fcchi complementation. In Zhiming Liu and Anders\u00a0P. Ravn, editors, Automated Technology for Verification and Analysis, 7th International Symposium, ATVA 2009, Macao, China, October 14-16, 2009. Proceedings, volume 5799 of Lecture Notes in Computer Science, pages 228\u2013243. Springer, 2009. https:\/\/doi.org\/10.1007\/978-3-642-04761-9_18.","DOI":"10.1007\/978-3-642-04761-9_18"},{"key":"5_CR25","doi-asserted-by":"publisher","unstructured":"Yonit Kesten and Amir Pnueli. A complete proof systems for QPTL. In Proceedings, 10th Annual IEEE Symposium on Logic in Computer Science, San Diego, California, USA, June 26-29, 1995, pages 2\u201312. IEEE Computer Society, 1995. https:\/\/doi.org\/10.1109\/LICS.1995.523239.","DOI":"10.1109\/LICS.1995.523239"},{"key":"5_CR26","doi-asserted-by":"publisher","unstructured":"Orna Kupferman and Moshe\u00a0Y. Vardi. Weak alternating automata are not that weak. ACM Trans. Comput. Log., 2(3):408\u2013429, 2001. https:\/\/doi.org\/10.1145\/377978.377993.","DOI":"10.1145\/377978.377993"},{"key":"5_CR27","doi-asserted-by":"publisher","unstructured":"Orna Kupferman and Moshe\u00a0Y. Vardi. Complementation constructions for nondeterministic automata on infinite words. In Nicolas Halbwachs and Lenore\u00a0D. Zuck, editors, Tools and Algorithms for the Construction and Analysis of Systems, 11th International Conference, TACAS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005, Proceedings, volume 3440 of Lecture Notes in Computer Science, pages 206\u2013221. Springer, 2005. https:\/\/doi.org\/10.1007\/978-3-540-31980-1_14.","DOI":"10.1007\/978-3-540-31980-1_14"},{"key":"5_CR28","doi-asserted-by":"publisher","unstructured":"Orna Kupferman and Moshe\u00a0Y. Vardi. From complementation to certification. Theor. Comput. Sci., 345(1):83\u2013100, 2005. https:\/\/doi.org\/10.1016\/j.tcs.2005.07.021.","DOI":"10.1016\/j.tcs.2005.07.021"},{"key":"5_CR29","doi-asserted-by":"publisher","unstructured":"Robert\u00a0P. Kurshan. 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.","DOI":"10.1016\/0022-0000(87)90036-5"},{"key":"5_CR30","doi-asserted-by":"publisher","unstructured":"Yong Li, Andrea Turrini, Weizhi Feng, Moshe\u00a0Y. Vardi, and Lijun Zhang. Divide-and-conquer determinization of B\u00fcchi automata based on SCC decomposition. In Sharon Shoham and Yakir Vizel, editors, Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part II, volume 13372 of Lecture Notes in Computer Science, pages 152\u2013173. Springer, 2022. https:\/\/doi.org\/10.1007\/978-3-031-13188-2_8.","DOI":"10.1007\/978-3-031-13188-2_8"},{"key":"5_CR31","doi-asserted-by":"crossref","unstructured":"Yong Li, Andrea Turrini, Lijun Zhang, and Sven Schewe. Learning to complement B\u00fcchi automata. In Proc. of VMCAI\u201918, pages 313\u2013335. Springer, 2018.","DOI":"10.1007\/978-3-319-73721-8_15"},{"key":"5_CR32","doi-asserted-by":"publisher","unstructured":"Yong Li, Moshe\u00a0Y. Vardi, and Lijun Zhang. On the power of unambiguity in B\u00fcchi complementation. In Jean-Francois Raskin and Davide Bresolin, editors, Proceedings 11th International Symposium on Games, Automata, Logics, and Formal Verification, Brussels, Belgium, September 21-22, 2020, volume 326 of Electronic Proceedings in Theoretical Computer Science, pages 182\u2013198. Open Publishing Association, 2020. https:\/\/doi.org\/10.4204\/EPTCS.326.12.","DOI":"10.4204\/EPTCS.326.12"},{"key":"5_CR33","unstructured":"Max Michel. Complementation is more difficult with automata on infinite words. CNET, Paris, 15, 1988."},{"key":"5_CR34","unstructured":"Satoru Miyano and Takeshi Hayashi. Alternating finite automata on omega-words. In Bruno Courcelle, editor, CAAP\u201984, 9th Colloquium on Trees in Algebra and Programming, Bordeaux, France, March 5-7, 1984, Proceedings, pages 195\u2013210. Cambridge University Press, 1984."},{"key":"5_CR35","doi-asserted-by":"crossref","unstructured":"Nir Piterman. From nondeterministic B\u00fcchi and Streett automata to deterministic parity automata. In Proc. of LICS\u201906, pages 255\u2013264. IEEE, 2006.","DOI":"10.1109\/LICS.2006.28"},{"key":"5_CR36","doi-asserted-by":"crossref","unstructured":"Shmuel Safra. On the complexity of $$\\omega $$-automata. In Proc. of FOCS\u201988, pages 319\u2013327. IEEE, 1988.","DOI":"10.1109\/SFCS.1988.21948"},{"key":"5_CR37","doi-asserted-by":"publisher","unstructured":"Shmuel Safra and Moshe\u00a0Y. Vardi. On $$\\omega $$-automata and temporal logic (preliminary report). In David\u00a0S. Johnson, editor, Proceedings of the 21st Annual ACM Symposium on Theory of Computing, May 14-17, 1989, Seattle, Washington, USA, pages 127\u2013137. ACM, 1989. https:\/\/doi.org\/10.1145\/73007.73019.","DOI":"10.1145\/73007.73019"},{"key":"5_CR38","doi-asserted-by":"publisher","unstructured":"Sven Schewe. B\u00fcchi 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\u00a03 of LIPIcs, pages 661\u2013672. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany, 2009. https:\/\/doi.org\/10.4230\/LIPIcs.STACS.2009.1854.","DOI":"10.4230\/LIPIcs.STACS.2009.1854"},{"key":"5_CR39","doi-asserted-by":"publisher","unstructured":"Sven Schewe and Thomas Varghese. Tight bounds for the determinisation and complementation of generalised B\u00fcchi automata. In Supratik Chakraborty and Madhavan Mukund, editors, Automated Technology for Verification and Analysis - 10th International Symposium, ATVA 2012, Thiruvananthapuram, India, October 3-6, 2012. Proceedings, volume 7561 of Lecture Notes in Computer Science, pages 42\u201356. Springer, 2012. https:\/\/doi.org\/10.1007\/978-3-642-33386-6_5.","DOI":"10.1007\/978-3-642-33386-6_5"},{"key":"5_CR40","doi-asserted-by":"publisher","unstructured":"Sven Schewe and Thomas Varghese. Determinising parity automata. In Erzs\u00e9bet Csuhaj-Varj\u00fa, Martin Dietzfelbinger, and Zolt\u00e1n \u00c9sik, editors, Mathematical Foundations of Computer Science 2014 - 39th International Symposium, MFCS 2014, Budapest, Hungary, August 25-29, 2014. Proceedings, Part I, volume 8634 of Lecture Notes in Computer Science, pages 486\u2013498. Springer, 2014. https:\/\/doi.org\/10.1007\/978-3-662-44522-8_41.","DOI":"10.1007\/978-3-662-44522-8_41"},{"key":"5_CR41","doi-asserted-by":"publisher","unstructured":"Sven Schewe and Thomas Varghese. Tight bounds for complementing parity automata. In Erzs\u00e9bet Csuhaj-Varj\u00fa, Martin Dietzfelbinger, and Zolt\u00e1n \u00c9sik, editors, Mathematical Foundations of Computer Science 2014 - 39th International Symposium, MFCS 2014, Budapest, Hungary, August 25-29, 2014. Proceedings, Part I, volume 8634 of Lecture Notes in Computer Science, pages 499\u2013510. Springer, 2014. https:\/\/doi.org\/10.1007\/978-3-662-44522-8_42.","DOI":"10.1007\/978-3-662-44522-8_42"},{"key":"5_CR42","doi-asserted-by":"crossref","unstructured":"A.\u00a0Prasad Sistla, Moshe\u00a0Y. Vardi, and Pierre Wolper. The Complementation Problem for B\u00fcchi Automata with Applications to Temporal Logic. Theoretical Computer Science, 49(2-3):217\u2013237, 1987.","DOI":"10.1016\/0304-3975(87)90008-9"},{"key":"5_CR43","doi-asserted-by":"publisher","unstructured":"Cong Tian, Wensheng Wang, and Zhenhua Duan. Making streett determinization tight. In Proceedings of the 35th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS \u201920, page 859-872, New York, NY, USA, 2020. Association for Computing Machinery. https:\/\/doi.org\/10.1145\/3373718.3394757.","DOI":"10.1145\/3373718.3394757"},{"key":"5_CR44","doi-asserted-by":"crossref","unstructured":"Moshe\u00a0Y. Vardi. The B\u00fcchi complementation saga. In Proc. of STACS\u201907, pages 12\u201322. Springer, 2007.","DOI":"10.1007\/978-3-540-70918-3_2"},{"key":"5_CR45","doi-asserted-by":"crossref","unstructured":"Qiqi Yan. Lower bounds for complementation of $$\\omega $$-automata via the full automata technique. In Michele Bugliesi, Bart Preneel, Vladimiro Sassone, and Ingo Wegener, editors, Automata, Languages and Programming, pages 589\u2013600, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg.","DOI":"10.1007\/11787006_50"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-90897-2_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T08:18:20Z","timestamp":1746001100000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-90897-2_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031908965","9783031908972"],"references-count":45,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-90897-2_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"1 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FoSSaCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/fossacs\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}