{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,11]],"date-time":"2025-09-11T19:43:06Z","timestamp":1757619786886,"version":"3.44.0"},"publisher-location":"Cham","reference-count":108,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030176006"},{"type":"electronic","value":"9783030176013"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-17601-3_2","type":"book-chapter","created":{"date-parts":[[2019,4,16]],"date-time":"2019-04-16T19:20:54Z","timestamp":1555442454000},"page":"38-98","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Learning B\u00fcchi Automata and Its Applications"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7301-9234","authenticated-orcid":false,"given":"Yong","family":"Li","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4343-9323","authenticated-orcid":false,"given":"Andrea","family":"Turrini","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2872-0336","authenticated-orcid":false,"given":"Yu-Fang","family":"Chen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3692-2088","authenticated-orcid":false,"given":"Lijun","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,4,14]]},"reference":[{"key":"2_CR1","unstructured":"RABIT tool. http:\/\/languageinclusion.org\/doku.php?id=tools"},{"key":"2_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-642-15375-4_6","volume-title":"CONCUR 2010 - Concurrency Theory","author":"F Aarts","year":"2010","unstructured":"Aarts, F., Vaandrager, F.W.: Learning I\/O automata. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 71\u201385. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15375-4_6"},{"key":"2_CR3","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). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_14"},{"key":"2_CR4","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). https:\/\/doi.org\/10.1007\/978-3-642-23217-6_13"},{"key":"2_CR5","doi-asserted-by":"crossref","unstructured":"Allred, J.D., Ultes-Nitsche, U.: A simple and optimal complementation algorithm for B\u00fcchi automata. In: LICS, pp. 46\u201355 (2018)","DOI":"10.1145\/3209108.3209138"},{"issue":"3","key":"2_CR6","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/BF01782772","volume":"2","author":"B Alpern","year":"1987","unstructured":"Alpern, B., Schneider, F.B.: Recognizing safety and liveness. Distrib. Comput. 2(3), 117\u2013126 (1987)","journal-title":"Distrib. Comput."},{"issue":"1","key":"2_CR7","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1145\/1047659.1040314","volume":"40","author":"Rajeev Alur","year":"2005","unstructured":"Alur, R., \u010cern\u1ef3, P., Madhusudan, P., Nam, W.: Synthesis of interface specifications for Java classes. In: POPL, pp. 98\u2013109 (2005)","journal-title":"ACM SIGPLAN Notices"},{"issue":"2","key":"2_CR8","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/0890-5401(87)90052-6","volume":"75","author":"D Angluin","year":"1987","unstructured":"Angluin, D.: Learning regular sets from queries and counterexamples. Inf. Comput. 75(2), 87\u2013106 (1987)","journal-title":"Inf. Comput."},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"Angluin, D., Boker, U., Fisman, D.: Families of DFAs as acceptors of omega-regular languages. In: MFCS, pp. 11:1\u201311:14 (2016)","DOI":"10.23638\/LMCS-14(1:15)2018"},{"key":"2_CR10","unstructured":"Angluin, D., Eisenstat, S., Fisman, D.: Learning regular languages via alternating automata. In: IJCAI, pp. 3308\u20133314 (2015)"},{"key":"2_CR11","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1016\/j.tcs.2016.07.031","volume":"650","author":"D Angluin","year":"2016","unstructured":"Angluin, D., Fisman, D.: Learning regular omega languages. Theor. Comput. Sci. 650, 57\u201372 (2016)","journal-title":"Theor. Comput. Sci."},{"key":"2_CR12","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(85)90148-3","volume":"39","author":"A Arnold","year":"1985","unstructured":"Arnold, A.: A syntactic congruence for rational $$\\omega $$-languages. Theor. Comput. Sci. 39, 333\u2013335 (1985)","journal-title":"Theor. Comput. Sci."},{"key":"2_CR13","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., et al.: The hanoi omega-automata format. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 479\u2013486. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_31"},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"Ben-Amram, A.M.: Size-change termination, monotonicity constraints and ranking functions. Log. Methods Comput. Sci. 6 (2010)","DOI":"10.2168\/LMCS-6(3:2)2010"},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"Ben-Amram, A.M., Genaim, S.: On the linear ranking problem for integer linear-constraint loops. In: POPL, pp. 51\u201362. ACM, New York (2013)","DOI":"10.1145\/2429069.2429078"},{"key":"2_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/978-3-319-21668-3_18","volume-title":"Computer Aided Verification","author":"AM Ben-Amram","year":"2015","unstructured":"Ben-Amram, A.M., Genaim, S.: Complexity of bradley-manna-sipma lexicographic ranking functions. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 304\u2013321. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21668-3_18"},{"key":"2_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"601","DOI":"10.1007\/978-3-319-63390-9_32","volume-title":"Computer Aided Verification","author":"AM Ben-Amram","year":"2017","unstructured":"Ben-Amram, A.M., Genaim, S.: On multiphase-linear ranking functions. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 601\u2013620. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_32"},{"key":"2_CR18","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: TACAS, pp. 193\u2013207 (1999)","DOI":"10.1007\/3-540-49059-0_14"},{"key":"2_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"770","DOI":"10.1007\/978-3-662-49674-9_49","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F Blahoudek","year":"2016","unstructured":"Blahoudek, F., Heizmann, M., Schewe, S., Strej\u010dek, J., Tsai, M.-H.: Complementing semi-deterministic B\u00fcchi automata. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 770\u2013787. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_49"},{"key":"2_CR20","unstructured":"Bollig, B., Habermehl, P., Kern, C., Leucker, M.: Angluin-style learning of NFA. In: IJCAI, pp. 1004\u20131009 (2009)"},{"key":"2_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"360","DOI":"10.1007\/978-3-642-14295-6_32","volume-title":"Computer Aided Verification","author":"B Bollig","year":"2010","unstructured":"Bollig, B., Katoen, J.-P., Kern, C., Leucker, M., Neider, D., Piegdon, D.R.: libalf: the automata learning framework. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 360\u2013364. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_32"},{"key":"2_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-662-54577-5_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C Borralleras","year":"2017","unstructured":"Borralleras, C., et al.: Proving termination through conditional termination. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 99\u2013117. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_6"},{"key":"2_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/11513988_48","volume-title":"Computer Aided Verification","author":"AR Bradley","year":"2005","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: Linear ranking with reachability. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 491\u2013504. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11513988_48"},{"key":"2_CR24","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). https:\/\/doi.org\/10.1007\/978-3-642-28729-9_10"},{"key":"2_CR25","unstructured":"B\u00fcchi, J.R.: On a decision method in restricted second order arithmetic. In: International Congress on Logic, Methodology and Philosophy of Science, pp. 1\u201311 (1962)"},{"key":"2_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"554","DOI":"10.1007\/3-540-58027-1_27","volume-title":"Mathematical Foundations of Programming Semantics","author":"H Calbrix","year":"1994","unstructured":"Calbrix, H., Nivat, M., Podelski, A.: Ultimately periodic words of rational $$\\omega $$-languages. In: Brookes, S., Main, M., Melton, A., Mislove, M., Schmidt, D. (eds.) MFPS 1993. LNCS, vol. 802, pp. 554\u2013566. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-58027-1_27"},{"key":"2_CR27","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/978-3-319-24953-7_9","volume-title":"Automated Technology for Verification and Analysis","author":"Martin Chapman","year":"2015","unstructured":"Chapman, M., Chockler, H., Kesseli, P., Kroening, D., Strichman, O., Tautschnig, M.: Learning the language of error. In: ATVA, pp. 114\u2013130 (2015)"},{"key":"2_CR28","doi-asserted-by":"crossref","unstructured":"Chen, Y.F., et al.: Advanced automata-based algorithms for program termination checking. In: PLDI, pp. 135\u2013150 (2018)","DOI":"10.1145\/3192366.3192405"},{"key":"2_CR29","doi-asserted-by":"crossref","unstructured":"Chen, Y.F., et al.: PAC learning-based verification and model synthesis. In: ICSE, pp. 714\u2013724 (2016)","DOI":"10.1145\/2884781.2884860"},{"issue":"2","key":"2_CR30","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/S0022-0000(74)80051-6","volume":"8","author":"Y Choueka","year":"1974","unstructured":"Choueka, Y.: Theories of automata on $$\\omega $$-tapes: a simplified approach. J. Comput. Syst. Sci. 8(2), 117\u2013141 (1974)","journal-title":"J. Comput. Syst. Sci."},{"key":"2_CR31","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/978-3-540-89439-1_13","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"EM Clarke","year":"2008","unstructured":"Clarke, E.M.: Model checking \u2013 my 27-year quest to overcome the state explosion problem. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 182\u2013182. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-89439-1_13"},{"key":"2_CR32","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8","volume-title":"Handbook of Model Checking","year":"2018","unstructured":"Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.): Handbook of Model Checking. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8"},{"key":"2_CR33","doi-asserted-by":"crossref","unstructured":"Clemente, L., Mayr, R.: Advanced automata minimization. In: Proceedings of POPL 2013, pp. 63\u201374. ACM (2013)","DOI":"10.1145\/2429069.2429079"},{"key":"2_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/3-540-36577-X_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"JM Cobleigh","year":"2003","unstructured":"Cobleigh, J.M., Giannakopoulou, D., P\u0102s\u0102reanu, C.S.: Learning assumptions for compositional verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 331\u2013346. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-36577-X_24"},{"issue":"1","key":"2_CR35","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/s10703-013-0186-4","volume":"43","author":"B Cook","year":"2013","unstructured":"Cook, B., Kroening, D., R\u00fcmmer, P., Wintersteiger, C.M.: Ranking function synthesis for bit-vector relations. Formal Methods Syst. Des. 43(1), 93\u2013120 (2013)","journal-title":"Formal Methods Syst. Des."},{"issue":"6","key":"2_CR36","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1145\/1133255.1134029","volume":"41","author":"Byron Cook","year":"2006","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: PLDI, pp. 415\u2013426. ACM, New York (2006)","journal-title":"ACM SIGPLAN Notices"},{"issue":"5","key":"2_CR37","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1145\/1941487.1941509","volume":"54","author":"B Cook","year":"2011","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Proving program termination. Commun. ACM 54(5), 88\u201398 (2011)","journal-title":"Commun. ACM"},{"key":"2_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/978-3-642-36742-7_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B Cook","year":"2013","unstructured":"Cook, B., See, A., Zuleger, F.: Ramsey vs. lexicographic termination proving. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 47\u201361. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_4"},{"key":"2_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-319-46520-3_8","volume-title":"Automated Technology for Verification and Analysis","author":"A Duret-Lutz","year":"2016","unstructured":"Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, \u00c9., Xu, L.: Spot 2.0 \u2014 a framework for LTL and $$\\omega $$-automata manipulation. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 122\u2013129. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46520-3_8"},{"key":"2_CR40","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Lei, C.: Modalities for model checking: branching time strikes back. In: POPL, pp. 84\u201396 (1985)","DOI":"10.1145\/318593.318620"},{"issue":"3","key":"2_CR41","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1016\/0167-6423(87)90036-0","volume":"8","author":"EA Emerson","year":"1987","unstructured":"Emerson, E.A., Lei, C.: Modalities for model checking: branching time logic strikes back. Sci. Comput. Program. 8(3), 275\u2013306 (1987)","journal-title":"Sci. Comput. Program."},{"key":"2_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-540-78800-3_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Farzan","year":"2008","unstructured":"Farzan, A., Chen, Y.-F., Clarke, E.M., Tsay, Y.-K., Wang, B.-Y.: Extending automated compositional verification to the full class of omega-regular languages. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 2\u201317. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_2"},{"key":"2_CR43","doi-asserted-by":"crossref","unstructured":"Feng, L., Kwiatkowska, M., Parker, D.: Compositional verification of probabilistic systems using learning. In: QEST, pp. 133\u2013142 (2010)","DOI":"10.1109\/QEST.2010.24"},{"key":"2_CR44","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1016\/j.ic.2014.12.021","volume":"245","author":"S Fogarty","year":"2015","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)","journal-title":"Inf. Comput."},{"key":"2_CR45","doi-asserted-by":"crossref","unstructured":"Fogarty, S., Kupferman, O., Wilke, T., Vardi, M.Y.: Unifying B\u00fcchi complementation constructions. Log. Methods Comput. Sci. 9(1) (2013)","DOI":"10.2168\/LMCS-9(1:13)2013"},{"key":"2_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/978-3-540-30476-0_10","volume-title":"Automated Technology for Verification and Analysis","author":"E Friedgut","year":"2004","unstructured":"Friedgut, E., Kupferman, O., Vardi, M.Y.: B\u00fcchi complementation made tighter. In: Wang, F. (ed.) ATVA 2004. LNCS, vol. 3299, pp. 64\u201378. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30476-0_10"},{"key":"2_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/978-3-642-39799-8_27","volume-title":"Computer Aided Verification","author":"P Ganty","year":"2013","unstructured":"Ganty, P., Genaim, S.: Proving termination starting from the end. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 397\u2013412. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_27"},{"key":"2_CR48","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10817-016-9388-y","volume":"58","author":"J Giesl","year":"2017","unstructured":"Giesl, J., et al.: Analyzing program termination and complexity automatically with AProVe. J. Autom. Reason. 58, 3\u201331 (2017)","journal-title":"J. Autom. Reason."},{"key":"2_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36387-4","volume-title":"Automata Logics, and Infinite Games","year":"2002","unstructured":"Gr\u00e4del, E., Thomas, W., Wilke, T. (eds.): Automata Logics, and Infinite Games. LNCS, vol. 2500. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-36387-4"},{"issue":"47","key":"2_CR50","doi-asserted-by":"publisher","first-page":"4029","DOI":"10.1016\/j.tcs.2010.07.008","volume":"411","author":"O Grinchtein","year":"2010","unstructured":"Grinchtein, O., Jonsson, B., Leucker, M.: Learning of event-recording automata. Theor. Comput. Sci. 411(47), 4029\u20134054 (2010)","journal-title":"Theor. Comput. Sci."},{"key":"2_CR51","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). https:\/\/doi.org\/10.1007\/978-3-540-39724-3_10"},{"key":"2_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/978-3-642-15769-1_19","volume-title":"Static Analysis","author":"WR Harris","year":"2010","unstructured":"Harris, W.R., Lal, A., Nori, A.V., Rajamani, S.K.: Alternation for termination. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 304\u2013319. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15769-1_19"},{"key":"2_CR53","unstructured":"van Heerdt, G., Sammartino, M., Silva, A.: CALF: categorical automata learning framework. In: CSL, pp. 29:1\u201329:24 (2017)"},{"key":"2_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/978-3-319-02444-8_26","volume-title":"Automated Technology for Verification and Analysis","author":"M Heizmann","year":"2013","unstructured":"Heizmann, M., Hoenicke, J., Leike, J., Podelski, A.: Linear ranking for linear lasso programs. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 365\u2013380. Springer, Cham (2013). https:\/\/doi.org\/10.1007\/978-3-319-02444-8_26"},{"key":"2_CR55","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). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_53"},{"key":"2_CR56","unstructured":"Hopcroft, J.E., Motwani, R., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation. Addison-Wesley Longman Publishing Co., Inc., Boston (2006)"},{"key":"2_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/978-3-642-27940-9_17","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"F Howar","year":"2012","unstructured":"Howar, F., Steffen, B., Jonsson, B., Cassel, S.: Inferring canonical register automata. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 251\u2013266. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-27940-9_17"},{"issue":"1\u20132","key":"2_CR58","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/s10994-013-5419-7","volume":"96","author":"M Isberner","year":"2014","unstructured":"Isberner, M., Howar, F., Steffen, B.: Learning register automata: from languages to program structures. Mach. Learn. 96(1\u20132), 65\u201398 (2014)","journal-title":"Mach. Learn."},{"key":"2_CR59","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-319-11164-3_26","volume-title":"Runtime Verification","author":"M Isberner","year":"2014","unstructured":"Isberner, M., Howar, F., Steffen, B.: The TTT algorithm: a redundancy-free approach to active automata learning. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 307\u2013322. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11164-3_26"},{"key":"2_CR60","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"487","DOI":"10.1007\/978-3-319-21690-4_32","volume-title":"Computer Aided Verification","author":"M Isberner","year":"2015","unstructured":"Isberner, M., Howar, F., Steffen, B.: The open-source LearnLib. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 487\u2013495. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_32"},{"key":"2_CR61","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). https:\/\/doi.org\/10.1007\/978-3-540-70575-8_59"},{"key":"2_CR62","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0304-3975(85)90043-X","volume":"36","author":"M Kaminski","year":"1985","unstructured":"Kaminski, M.: A classification of $$\\omega $$-regular languages. Theor. Comput. Sci. 36, 217\u2013229 (1985)","journal-title":"Theor. Comput. Sci."},{"key":"2_CR63","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/3897.001.0001","volume-title":"An Introduction to Computational Learning Theory","author":"MJ Kearns","year":"1994","unstructured":"Kearns, M.J., Vazirani, U.V.: An Introduction to Computational Learning Theory. MIT Press, Cambridge (1994)"},{"key":"2_CR64","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/978-3-642-14295-6_9","volume-title":"Computer Aided Verification","author":"D Kroening","year":"2010","unstructured":"Kroening, D., Sharygina, N., Tsitovich, A., Wintersteiger, C.M.: Termination analysis with compositional transition invariants. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 89\u2013103. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_9"},{"issue":"3","key":"2_CR65","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"},{"issue":"1","key":"2_CR66","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1016\/0022-0000(87)90036-5","volume":"35","author":"RP Kurshan","year":"1987","unstructured":"Kurshan, R.P.: Complementing deterministic B\u00fcchi automata in polynomial time. J. Comput. Syst. Sci. 35(1), 59\u201371 (1987)","journal-title":"J. Comput. Syst. Sci."},{"key":"2_CR67","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":"4","key":"2_CR68","doi-asserted-by":"publisher","first-page":"376","DOI":"10.1007\/BF01691063","volume":"3","author":"LH Landweber","year":"1969","unstructured":"Landweber, L.H.: Decision problems for $$\\omega $$-automata. Math. Syst. Theory 3(4), 376\u2013384 (1969)","journal-title":"Math. Syst. Theory"},{"issue":"6","key":"2_CR69","doi-asserted-by":"publisher","first-page":"489","DOI":"10.1145\/2813885.2737993","volume":"50","author":"Ton Chanh Le","year":"2015","unstructured":"Le, T.C., Qin, S., Chin, W.: Termination and non-termination specification inference. In: PLDI, pp. 489\u2013498. ACM, New York (2015)","journal-title":"ACM SIGPLAN Notices"},{"key":"2_CR70","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/978-3-642-31424-7_12","volume-title":"Computer Aided Verification","author":"W Lee","year":"2012","unstructured":"Lee, W., Wang, B.-Y., Yi, K.: Termination analysis with algorithmic learning. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 88\u2013104. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_12"},{"key":"2_CR71","doi-asserted-by":"crossref","unstructured":"Leike, J., Heizmann, M.: Ranking templates for linear loops. Log. Methods Comput. Sci. 11(1) (2015)","DOI":"10.2168\/LMCS-11(1:16)2015"},{"key":"2_CR72","unstructured":"Li, Y., Chen, Y., Zhang, L., Liu, D.: A novel learning algorithm for B\u00fcchi automata based on family of DFAs and classification trees. CoRR abs\/1610.07380 (2016). http:\/\/arxiv.org\/abs\/1610.07380"},{"key":"2_CR73","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/978-3-662-54577-5_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y Li","year":"2017","unstructured":"Li, Y., Chen, Y.-F., Zhang, L., Liu, D.: A novel learning algorithm for B\u00fcchi automata based on family of DFAs and classification trees. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 208\u2013226. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_12"},{"key":"2_CR74","first-page":"313","volume-title":"Lecture Notes in Computer Science","author":"Yong Li","year":"2017","unstructured":"Li, Y., Turrini, A., Zhang, L., Schewe, S.: Learning to complement B\u00fcchi automata. In: VMCAI, vol. 10747, pp. 313\u2013335 (2018)"},{"issue":"2","key":"2_CR75","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1109\/TSE.2013.57","volume":"40","author":"SW Lin","year":"2014","unstructured":"Lin, S.W., Andr\u00e9, E., Liu, Y., Sun, J., Dong, J.S.: Learning assumptions for compositional verification of timed systems. IEEE Trans. Softw. Eng. 40(2), 137\u2013153 (2014)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"2","key":"2_CR76","doi-asserted-by":"publisher","first-page":"316","DOI":"10.1006\/inco.1995.1070","volume":"118","author":"O Maler","year":"1995","unstructured":"Maler, O., Pnueli, A.: On the learnability of infinitary regular sets. Inf. Comput. 118(2), 316\u2013326 (1995)","journal-title":"Inf. Comput."},{"key":"2_CR77","doi-asserted-by":"crossref","unstructured":"Maler, O., Staiger, L.: On syntactic congruences for omega-languages. In: STACS, pp. 586\u2013594 (1993)","DOI":"10.1007\/3-540-56503-5_58"},{"key":"2_CR78","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer (1993)","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"2_CR79","doi-asserted-by":"crossref","unstructured":"Moerman, J., Sammartino, M., Silva, A., Klin, B., Szynwelski, M.: Learning nominal automata. In: POPL, pp. 613\u2013625 (2017)","DOI":"10.1145\/3009837.3009879"},{"issue":"POPL","key":"2_CR80","first-page":"26:1","volume":"2","author":"O Padon","year":"2018","unstructured":"Padon, O., Hoenicke, J., Losa, G., Podelski, A., Sagiv, M., Shoham, S.: Reducing liveness to safety in first-order logic. ACM Program. Lang. 2(POPL), 26:1\u201326:33 (2018)","journal-title":"ACM Program. Lang."},{"issue":"2","key":"2_CR81","first-page":"225","volume":"7","author":"D Peled","year":"2002","unstructured":"Peled, D., Vardi, M.Y., Yannakakis, M.: Black box checking. J. Automata Lang. Comb. 7(2), 225\u2013246 (2002)","journal-title":"J. Automata Lang. Comb."},{"key":"2_CR82","doi-asserted-by":"crossref","unstructured":"Piterman, N.: From nondeterministic B\u00fcchi and streett automata to deterministic parity automata. In: LICS, pp. 255\u2013264 (2006)","DOI":"10.1109\/LICS.2006.28"},{"key":"2_CR83","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/978-3-540-24622-0_20","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Podelski","year":"2004","unstructured":"Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 239\u2013251. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24622-0_20"},{"key":"2_CR84","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: Transition invariants. In: LICS, pp. 32\u201341. IEEE Computer Society, Washington, DC (2004)","DOI":"10.1109\/LICS.2004.1319598"},{"key":"2_CR85","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"314","DOI":"10.1007\/978-3-540-70545-1_31","volume-title":"Computer Aided Verification","author":"A Podelski","year":"2008","unstructured":"Podelski, A., Rybalchenko, A., Wies, T.: Heap assumptions on demand. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 314\u2013327. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-70545-1_31"},{"key":"2_CR86","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/978-3-642-28756-5_17","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C Popeea","year":"2012","unstructured":"Popeea, C., Rybalchenko, A.: Compositional termination proofs for multi-threaded programs. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 237\u2013251. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28756-5_17"},{"key":"2_CR87","doi-asserted-by":"crossref","unstructured":"Rivest, R.L., Schapire, R.E.: Inference of finite automata using homing sequences. In: STOC, pp. 411\u2013420 (1989)","DOI":"10.1145\/73007.73047"},{"key":"2_CR88","unstructured":"de Ruiter, J., Poll, E.: Protocol state fuzzing of TLS implementations. In: USENIX, pp. 193\u2013206 (2015)"},{"key":"2_CR89","doi-asserted-by":"crossref","unstructured":"Safra, S.: On the complexity of omega-automata. In: FOCS, pp. 319\u2013327 (1988)","DOI":"10.1109\/SFCS.1988.21948"},{"key":"2_CR90","unstructured":"Schewe, S.: B\u00fcchi complementation made tight. In: STACS. LIPIcs, vol. 3, pp. 661\u2013672 (2009)"},{"key":"2_CR91","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). https:\/\/doi.org\/10.1007\/978-3-642-00596-1_13"},{"key":"2_CR92","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1007\/978-3-319-41540-6_17","volume-title":"Computer Aided Verification","author":"S Sickert","year":"2016","unstructured":"Sickert, S., Esparza, J., Jaax, S., K\u0159et\u00ednsk\u00fd, J.: Limit-deterministic B\u00fcchi automata for linear temporal logic. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 312\u2013332. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_17"},{"key":"2_CR93","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 appplications to temporal logic. Theor. Comput. Sci. 49, 217\u2013237 (1987)","journal-title":"Theor. Comput. Sci."},{"issue":"8\/9","key":"2_CR94","first-page":"415","volume":"23","author":"L Staiger","year":"1987","unstructured":"Staiger, L.: Research in the theory of omega-languages. Elektronische Informationsverarbeitung und Kybernetik 23(8\/9), 415\u2013439 (1987)","journal-title":"Elektronische Informationsverarbeitung und Kybernetik"},{"key":"2_CR95","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/s10817-016-9389-x","volume":"58","author":"T Str\u00f6der","year":"2017","unstructured":"Str\u00f6der, T., et al.: Automatically proving termination and memory safety for programs with pointer arithmetic. J. Autom. Reason. 58, 33\u201365 (2017)","journal-title":"J. Autom. Reason."},{"key":"2_CR96","first-page":"133","volume-title":"Formal Models and Semantics","author":"Wolfgang THOMAS","year":"1990","unstructured":"Thomas, W.: Automata on infinite objects. In: Handbook of Theoretical Computer Science, vol. B: Formal Models and Sematics, chap. 4, pp. 133\u2013192 (1990)"},{"key":"2_CR97","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/978-3-642-59126-6_7","volume-title":"Handbook of Formal Languages","author":"W Thomas","year":"1997","unstructured":"Thomas, W.: Languages, automata, and logic. In: Rozenberg, G., Salomaa, A. (eds.) Handbook of Formal Languages, pp. 389\u2013455. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/978-3-642-59126-6_7"},{"key":"2_CR98","doi-asserted-by":"crossref","unstructured":"Tsai, M., Fogarty, S., Vardi, M.Y., Tsay, Y.: State of B\u00fcchi complementation. Log. Methods Comput. Sci. 10(4) (2014)","DOI":"10.2168\/LMCS-10(4:13)2014"},{"key":"2_CR99","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). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_62"},{"key":"2_CR100","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/978-3-642-19835-9_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y-K Tsay","year":"2011","unstructured":"Tsay, Y.-K., Tsai, M.-H., Chang, J.-S., Chang, Y.-W.: B\u00fcchi store: an open repository of B\u00fcchi automata. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 262\u2013266. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19835-9_23"},{"key":"2_CR101","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/978-3-662-49674-9_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C Urban","year":"2016","unstructured":"Urban, C., Gurfinkel, A., Kahsai, T.: Synthesizing ranking functions from bits and pieces. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 54\u201370. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_4"},{"key":"2_CR102","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"412","DOI":"10.1007\/978-3-642-54833-8_22","volume-title":"Programming Languages and Systems","author":"C Urban","year":"2014","unstructured":"Urban, C., Min\u00e9, A.: An abstract domain to infer ordinal-valued ranking functions. In: Shao, Z. (ed.) ESOP 2014. LNCS, vol. 8410, pp. 412\u2013431. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54833-8_22"},{"issue":"2","key":"2_CR103","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1145\/2967606","volume":"60","author":"F Vaandrager","year":"2017","unstructured":"Vaandrager, F.: Model learning. Commun. ACM 60(2), 86\u201395 (2017)","journal-title":"Commun. ACM"},{"key":"2_CR104","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/3-540-60915-6_6","volume-title":"Logics for Concurrency","author":"MY Vardi","year":"1996","unstructured":"Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Moller, F., Birtwistle, G. (eds.) Logics for Concurrency. LNCS, vol. 1043, pp. 238\u2013266. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-60915-6_6"},{"key":"2_CR105","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). https:\/\/doi.org\/10.1007\/978-3-540-70918-3_2"},{"key":"2_CR106","unstructured":"Vardi, M.Y., Wilke, T.: Automata: from logics to algorithms. In: Logic and Automata: History and Perspectives [in Honor of Wolfgang Thomas], pp. 629\u2013736 (2008)"},{"key":"2_CR107","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1007\/978-3-642-19811-3_22","volume-title":"Fundamental Approaches to Software Engineering","author":"F Wang","year":"2011","unstructured":"Wang, F., Wu, J.-H., Huang, C.-H., Chang, K.-H.: Evolving a test oracle in black-box testing. In: Giannakopoulou, D., Orejas, F. (eds.) FASE 2011. LNCS, vol. 6603, pp. 310\u2013325. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19811-3_22"},{"key":"2_CR108","doi-asserted-by":"crossref","unstructured":"Yan, Q.: Lower bounds for complementation of $$\\omega $$-automata via the full automata technique. Log. Methods Comput. Sci. 4(1:5) (2008)","DOI":"10.2168\/LMCS-4(1:5)2008"}],"container-title":["Lecture Notes in Computer Science","Engineering Trustworthy Software Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-17601-3_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,8]],"date-time":"2025-09-08T01:12:59Z","timestamp":1757293979000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-17601-3_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030176006","9783030176013"],"references-count":108,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-17601-3_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"14 April 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SETSS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Summer School on Engineering Trustworthy Software Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Chongqing","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 April 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 April 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"setss2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.swu-rise.net.cn\/SETSS2018\/SETSS2018.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Open","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Easychair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"100% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"1-2","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"1-2","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}