{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:11:46Z","timestamp":1760202706482,"version":"3.41.0"},"publisher-location":"Berlin, Heidelberg","reference-count":37,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662496732"},{"type":"electronic","value":"9783662496749"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-662-49674-9_49","type":"book-chapter","created":{"date-parts":[[2016,4,8]],"date-time":"2016-04-08T18:49:00Z","timestamp":1460141340000},"page":"770-787","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":16,"title":["Complementing Semi-deterministic B\u00fcchi Automata"],"prefix":"10.1007","author":[{"given":"Franti\u0161ek","family":"Blahoudek","sequence":"first","affiliation":[]},{"given":"Matthias","family":"Heizmann","sequence":"additional","affiliation":[]},{"given":"Sven","family":"Schewe","sequence":"additional","affiliation":[]},{"given":"Jan","family":"Strej\u010dek","sequence":"additional","affiliation":[]},{"given":"Ming-Hsien","family":"Tsai","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,4,9]]},"reference":[{"key":"49_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/978-3-642-39176-7_6","volume-title":"Model Checking Software","author":"T Babiak","year":"2013","unstructured":"Babiak, T., Badie, T., Duret-Lutz, A., K\u0159et\u00ednsk\u00fd, M., Strej\u010dek, J.: Compositional approach to suspension and other improvements to LTL translation. In: Bartocci, E., Ramakrishnan, C.R. (eds.) SPIN 2013. LNCS, vol. 7976, pp. 81\u201398. Springer, Heidelberg (2013)"},{"key":"49_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"479","DOI":"10.1007\/978-3-319-21690-4_31","volume-title":"Computer Aided Verification","author":"T Babiak","year":"2015","unstructured":"Babiak, T., Blahoudek, F., Duret-Lutz, A., Klein, J., K\u0159et\u00ednsk\u00fd, J., M\u00fcller, D., Parker, D., Strej\u010dek, J.: The Hanoi omega-automata format. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 479\u2013486. Springer, Heidelberg (2015)"},{"key":"49_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-642-36742-7_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Benedikt","year":"2013","unstructured":"Benedikt, M., Lenhardt, R., Worrell, J.: LTL model checking of interval Markov chains. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 32\u201346. Springer, Heidelberg (2013)"},{"key":"49_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"401","DOI":"10.1007\/978-3-662-46681-0_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Beyer","year":"2015","unstructured":"Beyer, D.: Software verification and verifiable witnesses. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 401\u2013416. Springer, Heidelberg (2015)"},{"key":"49_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1007\/978-3-642-28729-9_10","volume-title":"Foundations of Software Science and Computational Structures","author":"S Breuers","year":"2012","unstructured":"Breuers, S., L\u00f6ding, C., Olschewski, J.: Improved Ramsey-based B\u00fcchi complementation. In: Birkedal, L. (ed.) FOSSACS 2012. LNCS, vol. 7213, pp. 150\u2013164. Springer, Heidelberg (2012)"},{"key":"49_CR6","unstructured":"B\u00fcchi, J.R.: On a decision method in restricted second order arithmetic. In: CLMpPS 1960, pp. 1\u201311. Stanford University Press (1962)"},{"key":"49_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/978-3-540-27813-9_15","volume-title":"Computer Aided Verification","author":"D Bustan","year":"2004","unstructured":"Bustan, D., Rubin, S., Vardi, M.Y.: Verifying $$\\omega $$ -regular properties of Markov chains. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 189\u2013201. Springer, Heidelberg (2004)"},{"issue":"4","key":"49_CR8","doi-asserted-by":"publisher","first-page":"857","DOI":"10.1145\/210332.210339","volume":"42","author":"C Courcoubetis","year":"1995","unstructured":"Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. J. ACM 42(4), 857\u2013907 (1995)","journal-title":"J. ACM"},{"key":"49_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-319-21690-4_4","volume-title":"Computer Aided Verification","author":"D Dietsch","year":"2015","unstructured":"Dietsch, D., Heizmann, M., Langenfeld, V., Podelski, A.: Fairness modulo theory: a new approach to LTL software model checking. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 49\u201366. Springer, Heidelberg (2015)"},{"key":"49_CR10","doi-asserted-by":"crossref","unstructured":"Duret-Lutz, A., Poitrenaud, D., SPOT: An extensible model checking library using transition-based generalized B\u00fcchi automata. In: MASCOTS 2004, pp. 76\u201383. IEEE Computer Society (2004)","DOI":"10.1109\/MASCOT.2004.1348184"},{"issue":"1","key":"49_CR11","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-9(1:13)2013","volume":"9","author":"S Fogarty","year":"2013","unstructured":"Fogarty, S., Kupferman, O., Wilke, T., Vardi, M.Y.: Unifying B\u00fcchi complementation constructions. Logical Methods Comput. Sci. 9(1), 1\u201325 (2013)","journal-title":"Logical Methods Comput. Sci."},{"issue":"4","key":"49_CR12","doi-asserted-by":"publisher","first-page":"851","DOI":"10.1142\/S0129054106004145","volume":"17","author":"E Friedgut","year":"2006","unstructured":"Friedgut, E., Kupferman, O., Vardi, M.Y.: B\u00fcchi complementation made tighter. Int. J. Found. Comput. Sci. 17(4), 851\u2013868 (2006)","journal-title":"Int. J. Found. Comput. Sci."},{"key":"49_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/978-3-540-39724-3_10","volume-title":"Correct Hardware Design and Verification Methods","author":"S Gurumurthy","year":"2003","unstructured":"Gurumurthy, S., Kupferman, O., Somenzi, F., Vardi, M.Y.: On complementing nondeterministic B\u00fcchi automata. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 96\u2013110. Springer, Heidelberg (2003)"},{"key":"49_CR14","unstructured":"Hahn, E.M., Li, G., Schewe, S., Turrini, A., Zhang, L.: Lazy probabilistic model checking without determinisation. In: CONCUR 2015. LIPIcs, vol. 42, pp. 354\u2013367. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2015)"},{"key":"49_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"797","DOI":"10.1007\/978-3-319-08867-9_53","volume-title":"Computer Aided Verification","author":"M Heizmann","year":"2014","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Termination analysis by learning terminating programs. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 797\u2013813. Springer, Heidelberg (2014)"},{"key":"49_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"724","DOI":"10.1007\/978-3-540-70575-8_59","volume-title":"Automata, Languages and Programming","author":"D K\u00e4hler","year":"2008","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.) ICALP 2008, Part I. LNCS, vol. 5125, pp. 724\u2013735. Springer, Heidelberg (2008)"},{"issue":"2","key":"49_CR17","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1145\/377978.377993","volume":"2","author":"O Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. ACM Trans. Comput. Logic 2(2), 408\u2013429 (2001)","journal-title":"ACM Trans. Comput. Logic"},{"key":"49_CR18","volume-title":"Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach","author":"RP Kurshan","year":"1994","unstructured":"Kurshan, R.P.: Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, Princeton (1994)"},{"issue":"5","key":"49_CR19","doi-asserted-by":"publisher","first-page":"521","DOI":"10.1016\/S0019-9958(66)80013-X","volume":"9","author":"R McNaughton","year":"1966","unstructured":"McNaughton, R.: Testing and generating infinite sequences by a finite automaton. Inf. Control 9(5), 521\u2013530 (1966)","journal-title":"Inf. Control"},{"key":"49_CR20","unstructured":"Michel, M.: Complementation is more difficult with automata on infinite words. Technical report, CNET, Paris (Manuscript) (1988)"},{"issue":"3","key":"49_CR21","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1016\/0304-3975(84)90049-5","volume":"32","author":"S Miyano","year":"1984","unstructured":"Miyano, S., Hayashi, T.: Alternating finite automata on $$\\omega $$ -words. Theor. Comput. Sci. 32(3), 321\u2013330 (1984)","journal-title":"Theor. Comput. Sci."},{"key":"49_CR22","doi-asserted-by":"crossref","unstructured":"Muller, D.E.: Infinite sequences and finite machines. In: FOCS 1963, pp. 3\u201316. IEEE Computer Society Press (1963)","DOI":"10.1109\/SWCT.1963.8"},{"issue":"3","key":"49_CR23","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0304-3975(86)90136-2","volume":"47","author":"J-P P\u00e9cuchet","year":"1986","unstructured":"P\u00e9cuchet, J.-P.: On the complementation of B\u00fcchi automata. Theor. Comput. Sci. 47(3), 95\u201398 (1986)","journal-title":"Theor. Comput. Sci."},{"key":"49_CR24","doi-asserted-by":"crossref","unstructured":"Piterman, N.: From nondeterministic B\u00fcchi and Streett automata to deterministic parity automata. Logical Methods Comput. Sci. 3(3:5) (2007)","DOI":"10.2168\/LMCS-3(3:5)2007"},{"key":"49_CR25","doi-asserted-by":"crossref","unstructured":"Safra, S.: On the complexity of omega-automata. In: FOCS 1988, pp. 319\u2013327. IEEE Computer Society (1988)","DOI":"10.1109\/SFCS.1988.21948"},{"key":"49_CR26","doi-asserted-by":"crossref","unstructured":"Sakoda, W.J., Sipser, M.: Non-determinism and the size of two-way automata. In STOC 1978, pp. 274\u2013286. ACM Press (1978)","DOI":"10.1145\/800133.804357"},{"key":"49_CR27","unstructured":"Schewe, S.: B\u00fcchi complementation made tight. In: STACS 2009. LIPIcs, vol. 3, pp. 661\u2013672. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2009)"},{"key":"49_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-642-00596-1_13","volume-title":"Foundations of Software Science and Computational Structures","author":"S Schewe","year":"2009","unstructured":"Schewe, S.: Tighter bounds for the determinisation of B\u00fcchi automata. In: de Alfaro, L. (ed.) FOSSACS 2009. LNCS, vol. 5504, pp. 167\u2013181. Springer, Heidelberg (2009)"},{"key":"49_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/978-3-642-33386-6_5","volume-title":"Automated Technology for Verification and Analysis","author":"S Schewe","year":"2012","unstructured":"Schewe, S., Varghese, T.: Tight bounds for the determinisation and complementation of generalised B\u00fcchi automata. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol. 7561, pp. 42\u201356. Springer, Heidelberg (2012)"},{"key":"49_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"499","DOI":"10.1007\/978-3-662-44522-8_42","volume-title":"Mathematical Foundations of Computer Science 2014","author":"S Schewe","year":"2014","unstructured":"Schewe, S., Varghese, T.: Tight bounds for complementing parity automata. In: Csuhaj-Varj\u00fa, E., Dietzfelbinger, M., \u00c9sik, Z. (eds.) MFCS 2014, Part I. LNCS, vol. 8634, pp. 499\u2013510. Springer, Heidelberg (2014)"},{"issue":"3","key":"49_CR31","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0304-3975(87)90008-9","volume":"49","author":"AP Sistla","year":"1987","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(3), 217\u2013239 (1987)","journal-title":"Theor. Comput. Sci."},{"key":"49_CR32","doi-asserted-by":"crossref","unstructured":"Tsai, M.-H., Fogarty, S., Vardi, M.Y., Tsay, Y.: State of B\u00fcchi complementation. Logical Methods Comput. Sci. 10(4:13) (2014)","DOI":"10.2168\/LMCS-10(4:13)2014"},{"key":"49_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"883","DOI":"10.1007\/978-3-642-39799-8_62","volume-title":"Computer Aided Verification","author":"M-H Tsai","year":"2013","unstructured":"Tsai, M.-H., Tsay, Y.-K., Hwang, Y.-S.: GOAL for Games, omega-automata, and logics. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 883\u2013889. Springer, Heidelberg (2013)"},{"key":"49_CR34","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state programs. In: FOCS 1985, pp. 327\u2013338. IEEE Computer Society (1985)","DOI":"10.1109\/SFCS.1985.12"},{"key":"49_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1007\/978-3-540-70918-3_2","volume-title":"STACS 2007","author":"MY Vardi","year":"2007","unstructured":"Vardi, M.Y.: The B\u00fcchi complementation saga. In: Thomas, W., Weil, P. (eds.) STACS 2007. LNCS, vol. 4393, pp. 12\u201322. Springer, Heidelberg (2007)"},{"key":"49_CR36","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification (preliminary report). In: LICS 1986, pp. 332\u2013344. IEEE Computer Society (1986)"},{"key":"49_CR37","doi-asserted-by":"crossref","unstructured":"Yan, Q., Lower bounds for complementation of omega-automata via the full automata technique. Logical Methods Comput. Sci. 4(1: 5), 1\u201320 (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":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-49674-9_49","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,2]],"date-time":"2025-06-02T08:28:43Z","timestamp":1748852923000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49674-9_49"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783662496732","9783662496749"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49674-9_49","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"9 April 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}