{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,10]],"date-time":"2026-06-10T07:18:19Z","timestamp":1781075899547,"version":"3.54.1"},"publisher-location":"Cham","reference-count":41,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030341749","type":"print"},{"value":"9783030341756","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"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":[[2019]]},"DOI":"10.1007\/978-3-030-34175-6_23","type":"book-chapter","created":{"date-parts":[[2019,11,18]],"date-time":"2019-11-18T00:01:29Z","timestamp":1574035289000},"page":"447-467","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Simulations in Rank-Based B\u00fcchi Automata Complementation"],"prefix":"10.1007","author":[{"given":"Yu-Fang","family":"Chen","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Vojt\u011bch","family":"Havlena","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ond\u0159ej","family":"Leng\u00e1l","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2019,11,18]]},"reference":[{"key":"23_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/978-3-642-14295-6_14","volume-title":"Computer Aided Verification","author":"PA Abdulla","year":"2010","unstructured":"Abdulla, P.A., et al.: Simulation subsumption in Ramsey-based B\u00fcchi automata universality and inclusion testing. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 132\u2013147. Springer, Heidelberg (2010). \nhttps:\/\/doi.org\/10.1007\/978-3-642-14295-6_14"},{"key":"23_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-642-23217-6_13","volume-title":"CONCUR 2011 \u2013 Concurrency Theory","author":"PA Abdulla","year":"2011","unstructured":"Abdulla, P.A., et al.: Advanced Ramsey-based B\u00fcchi automata inclusion testing. In: Katoen, J.-P., K\u00f6nig, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 187\u2013202. Springer, Heidelberg (2011). \nhttps:\/\/doi.org\/10.1007\/978-3-642-23217-6_13"},{"key":"23_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/978-3-642-12002-2_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"PA Abdulla","year":"2010","unstructured":"Abdulla, P.A., Chen, Y.-F., Hol\u00edk, L., Mayr, R., Vojnar, T.: When simulation meets antichains. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 158\u2013174. Springer, Heidelberg (2010). \nhttps:\/\/doi.org\/10.1007\/978-3-642-12002-2_14"},{"key":"23_CR4","doi-asserted-by":"crossref","unstructured":"Allred, J.D., Ultes-Nitsche, U.: A Simple and optimal complementation algorithm for B\u00fcchi automata. In: Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science, pp. 46\u201355. ACM (2018)","DOI":"10.1145\/3209108.3209138"},{"key":"23_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). \nhttps:\/\/doi.org\/10.1007\/978-3-642-28729-9_10"},{"key":"23_CR6","unstructured":"B\u00fcchi, J.R.: On a decision method in restricted second order arithmetic. In: Proceedings of International Congress on Logic, Method, and Philosophy of Science 1960. Stanford University Press, Stanford (1962)"},{"issue":"2","key":"23_CR7","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1145\/635499.635502","volume":"4","author":"D Bustan","year":"2003","unstructured":"Bustan, D., Grumberg, O.: Simulation-based minimization. ACM Trans. Comput. Logic 4(2), 181\u2013206 (2003)","journal-title":"ACM Trans. Comput. Logic"},{"key":"23_CR8","doi-asserted-by":"crossref","unstructured":"C\u00e9c\u00e9, G.: Foundation for a series of efficient simulation algorithms. In: Proceedings of LICS 2017, pp. 1\u201312 (2017)","DOI":"10.1109\/LICS.2017.8005069"},{"key":"23_CR9","doi-asserted-by":"crossref","unstructured":"Chen, Y., et al.: Advanced automata-based algorithms for program termination checking. In: Proceedings of PLDI 2018, pp. 135\u2013150. ACM (2018)","DOI":"10.1145\/3296979.3192405"},{"key":"23_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-642-22012-8_20","volume-title":"Automata, Languages and Programming","author":"L Clemente","year":"2011","unstructured":"Clemente, L.: B\u00fcchi automata can have smaller quotients. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP 2011. LNCS, vol. 6756, pp. 258\u2013270. Springer, Heidelberg (2011). \nhttps:\/\/doi.org\/10.1007\/978-3-642-22012-8_20"},{"key":"23_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/3-540-55179-4_25","volume-title":"Computer Aided Verification","author":"DL Dill","year":"1992","unstructured":"Dill, D.L., Hu, A.J., Wong-Toi, H.: Checking for language inclusion using simulation preorders. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol. 575, pp. 255\u2013265. Springer, Heidelberg (1992). \nhttps:\/\/doi.org\/10.1007\/3-540-55179-4_25"},{"issue":"5","key":"23_CR12","doi-asserted-by":"publisher","first-page":"1159","DOI":"10.1137\/S0097539703420675","volume":"34","author":"K Etessami","year":"2005","unstructured":"Etessami, K., Wilke, T., Schuller, R.: Fair simulation relations, parity games, and state space reduction for B\u00fcchi automata. SIAM J. Comput. 34(5), 1159\u20131175 (2005)","journal-title":"SIAM J. Comput."},{"key":"23_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/3-540-45694-5_10","volume-title":"CONCUR 2002 \u2014 Concurrency Theory","author":"K Etessami","year":"2002","unstructured":"Etessami, K.: A hierarchy of polynomial-time computable simulations for automata. In: Brim, L., K\u0159et\u00ednsk\u00fd, M., Ku\u010dera, A., Jan\u010dar, P. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 131\u2013144. Springer, Heidelberg (2002). \nhttps:\/\/doi.org\/10.1007\/3-540-45694-5_10"},{"key":"23_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/978-3-642-00768-2_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Fogarty","year":"2009","unstructured":"Fogarty, S., Vardi, M.Y.: B\u00fcchi complementation and size-change termination. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 16\u201330. Springer, Heidelberg (2009). \nhttps:\/\/doi.org\/10.1007\/978-3-642-00768-2_2"},{"key":"23_CR15","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.: B\u00fcchi complementation made tighter. Int. J. Found. Comput. Sci. 17, 851\u2013868 (2006)","journal-title":"Int. J. Found. Comput. Sci."},{"issue":"1","key":"23_CR16","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1016\/j.tcs.2005.01.016","volume":"338","author":"C Fritz","year":"2005","unstructured":"Fritz, C., Wilke, T.: Simulation relations for alternating B\u00fcchi automata. Theor. Comput. Sci. 338(1), 275\u2013314 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"23_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/978-3-540-70844-5_17","volume-title":"Implementation and Applications of Automata","author":"R Glabbeek van","year":"2008","unstructured":"van Glabbeek, R., Ploeger, B.: Five determinisation algorithms. In: Ibarra, O.H., Ravikumar, B. (eds.) CIAA 2008. LNCS, vol. 5148, pp. 161\u2013170. Springer, Heidelberg (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-70844-5_17"},{"key":"23_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"610","DOI":"10.1007\/3-540-45657-0_51","volume-title":"Computer Aided Verification","author":"S Gurumurthy","year":"2002","unstructured":"Gurumurthy, S., Bloem, R., Somenzi, F.: Fair simulation minimization. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 610\u2013623. Springer, Heidelberg (2002). \nhttps:\/\/doi.org\/10.1007\/3-540-45657-0_51"},{"key":"23_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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, Cham (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-319-08867-9_53"},{"key":"23_CR20","unstructured":"Henzinger, M.R., Henzinger, T.A., Kopke, P.W.: Computing simulations on finite and infinite graphs. In: Proceedings of FOCS 1995, pp. 453\u2013462. IEEE Computer Society (1995)"},{"issue":"1","key":"23_CR21","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1006\/inco.2001.3085","volume":"173","author":"TA Henzinger","year":"2002","unstructured":"Henzinger, T.A., Kupferman, O., Rajamani, S.K.: Fair simulation. Inf. Comput. 173(1), 64\u201381 (2002)","journal-title":"Inf. Comput."},{"key":"23_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-540-27812-2_11","volume-title":"Theory Is Forever","author":"L Ilie","year":"2004","unstructured":"Ilie, L., Navarro, G., Yu, S.: On NFA reductions. In: Karhum\u00e4ki, J., Maurer, H., P\u0103un, G., Rozenberg, G. (eds.) Theory Is Forever. LNCS, vol. 3113, pp. 112\u2013124. Springer, Heidelberg (2004). \nhttps:\/\/doi.org\/10.1007\/978-3-540-27812-2_11"},{"key":"23_CR23","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. LNCS, vol. 5125, pp. 724\u2013735. Springer, Heidelberg (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-70575-8_59"},{"issue":"3","key":"23_CR24","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(3), 408\u2013429 (2001)","journal-title":"ACM Trans. Comput. Logic"},{"key":"23_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/978-3-319-73721-8_15","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"Y Li","year":"2018","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. LNCS, vol. 10747, pp. 313\u2013335. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-319-73721-8_15"},{"issue":"1","key":"23_CR26","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1145\/2480359.2429079","volume":"48","author":"Richard Mayr","year":"2013","unstructured":"Mayr, R., Clemente, L.: Advanced automata minimization. In: Proceedings of POPL 2013, pp. 63\u201374 (2013)","journal-title":"ACM SIGPLAN Notices"},{"key":"23_CR27","first-page":"12:1","volume":"15","author":"R Mayr","year":"2019","unstructured":"Mayr, R., Clemente, L.: Efficient reduction of nondeterministic automata with application to language inclusion testing. Logical Methods Comput. Sci. 15, 12:1\u201312:73 (2019)","journal-title":"Logical Methods Comput. Sci."},{"key":"23_CR28","unstructured":"Michel, M.: Complementation is more difficult with automata on infinite words. In: CNET, Paris, vol. 15 (1988)"},{"key":"23_CR29","doi-asserted-by":"crossref","unstructured":"Piterman, N.: From nondeterministic B\u00fcchi and Streett automata to deterministic parity automata. In: Proceedings of LICS 2006. pp. 255\u2013264. IEEE (2006)","DOI":"10.2168\/LMCS-3(3:5)2007"},{"key":"23_CR30","doi-asserted-by":"crossref","unstructured":"Ranzato, F., Tapparo, F.: A new efficient simulation equivalence algorithm. In: Proceedings of LICS 2007, pp. 171\u2013180 (2007)","DOI":"10.1109\/LICS.2007.8"},{"issue":"1","key":"23_CR31","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.ic.2009.06.002","volume":"208","author":"F Ranzato","year":"2010","unstructured":"Ranzato, F., Tapparo, F.: An efficient simulation algorithm based on abstract interpretation. Inf. Comput. 208(1), 1\u201322 (2010)","journal-title":"Inf. Comput."},{"key":"23_CR32","doi-asserted-by":"crossref","unstructured":"Safra, S.: On the complexity of $$\\omega $$-automata. In: Proceedings of FOCS 1988, pp. 319\u2013327. IEEE (1988)","DOI":"10.1109\/SFCS.1988.21948"},{"key":"23_CR33","unstructured":"Schewe, S.: B\u00fcchi complementation made tight. In: Proceedings of STACS 2009, pp. 661\u2013672. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2009)"},{"issue":"2\u20133","key":"23_CR34","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(2\u20133), 217\u2013237 (1987)","journal-title":"Theor. Comput. Sci."},{"key":"23_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1007\/BFb0015772","volume-title":"Automata, Languages and Programming","author":"AP Sistla","year":"1985","unstructured":"Sistla, A.P., Vardi, M.Y., Wolper, P.: The complementation problem for B\u00fcchi automata with applications to temporal logic. In: Brauer, W. (ed.) ICALP 1985. LNCS, vol. 194, pp. 465\u2013474. Springer, Heidelberg (1985). \nhttps:\/\/doi.org\/10.1007\/BFb0015772"},{"key":"23_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/10722167_21","volume-title":"Computer Aided Verification","author":"F Somenzi","year":"2000","unstructured":"Somenzi, F., Bloem, R.: Efficient B\u00fcchi automata from LTL formulae. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 248\u2013263. Springer, Heidelberg (2000). \nhttps:\/\/doi.org\/10.1007\/10722167_21"},{"key":"23_CR37","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1007\/11591191_28","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"D Tabakov","year":"2005","unstructured":"Tabakov, D., Vardi, M.Y.: Experimental evaluation of classical automata constructions. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3835, pp. 396\u2013411. Springer, Heidelberg (2005). \nhttps:\/\/doi.org\/10.1007\/11591191_28"},{"key":"23_CR38","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). \nhttps:\/\/doi.org\/10.1007\/978-3-540-70918-3_2"},{"key":"23_CR39","first-page":"629","volume":"2","author":"MY Vardi","year":"2008","unstructured":"Vardi, M.Y., Wilke, T.: Automata: from logics to algorithms. Logic Automata 2, 629\u2013736 (2008)","journal-title":"Logic Automata"},{"key":"23_CR40","first-page":"1","volume":"9","author":"MY Vardi","year":"2013","unstructured":"Vardi, M.Y., Wilke, T., Kupferman, O., Fogarty, S.J.: Unifying B\u00fcchi complementation constructions. Logical Methods Comput. Sci. 9, 1\u201325 (2013)","journal-title":"Logical Methods Comput. Sci."},{"key":"23_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"589","DOI":"10.1007\/11787006_50","volume-title":"Automata, Languages and Programming","author":"Q Yan","year":"2006","unstructured":"Yan, Q.: Lower bounds for complementation of $$\\omega $$-automata via the full automata technique. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol. 4052, pp. 589\u2013600. Springer, Heidelberg (2006). \nhttps:\/\/doi.org\/10.1007\/11787006_50"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-34175-6_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,11,18]],"date-time":"2019-11-18T00:07:46Z","timestamp":1574035666000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-34175-6_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030341749","9783030341756"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-34175-6_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"18 November 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"APLAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Asian Symposium on Programming Languages and Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Nusa Dua, Bali","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Indonesia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 December 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 December 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"aplas2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/aplas-2019","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}