{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,15]],"date-time":"2026-05-15T18:23:01Z","timestamp":1778869381471,"version":"3.51.4"},"publisher-location":"Cham","reference-count":43,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783031131875","type":"print"},{"value":"9783031131882","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,8,6]],"date-time":"2022-08-06T00:00:00Z","timestamp":1659744000000},"content-version":"vor","delay-in-days":217,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The determinization of a nondeterministic B\u00fcchi automaton (NBA) is a fundamental construction of automata theory, with applications to probabilistic verification and reactive synthesis. The standard determinization constructions, such as the ones based on the Safra-Piterman\u2019s approach, work on the whole NBA. In this work we propose a divide-and-conquer determinization approach. To this end, we first classify the strongly connected components (SCCs) of the given NBA as inherently weak, deterministic accepting, and nondeterministic accepting. We then present how to determinize each type of SCC <jats:italic>independently<\/jats:italic> from the others; this results in an easier handling of the determinization algorithm that takes advantage of the structure of that SCC. Once all SCCs have been determinized, we show how to compose them so to obtain the final equivalent deterministic Emerson-Lei automaton, which can be converted into a deterministic Rabin automaton without blow-up of states and transitions. We implement our algorithm in our tool <jats:sc>COLA<\/jats:sc> and empirically evaluate <jats:sc>COLA<\/jats:sc> with the state-of-the-art tools <jats:sc>Spot<\/jats:sc> and <jats:sc>Owl<\/jats:sc> on a large set of benchmarks from the literature. The experimental results show that our prototype <jats:sc>COLA<\/jats:sc> outperforms <jats:sc>Spot<\/jats:sc> and <jats:sc>Owl<\/jats:sc> regarding the number of states and transitions.<\/jats:p>","DOI":"10.1007\/978-3-031-13188-2_8","type":"book-chapter","created":{"date-parts":[[2022,8,5]],"date-time":"2022-08-05T08:16:57Z","timestamp":1659687417000},"page":"152-173","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Divide-and-Conquer Determinization of\u00a0B\u00fcchi Automata Based on\u00a0SCC Decomposition"],"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-0710-223X","authenticated-orcid":false,"given":"Weizhi","family":"Feng","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0661-5773","authenticated-orcid":false,"given":"Moshe Y.","family":"Vardi","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":[[2022,8,6]]},"reference":[{"key":"8_CR1","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":"8_CR2","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"issue":"1","key":"8_CR3","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10009-017-0469-y","volume":"21","author":"D Beyer","year":"2017","unstructured":"Beyer, D., L\u00f6we, S., Wendler, P.: Reliable benchmarking: requirements and solutions. Int. J. Softw. Tools Technol. Transfer 21(1), 1\u201329 (2017). https:\/\/doi.org\/10.1007\/s10009-017-0469-y","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"8_CR4","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":"8_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"611","DOI":"10.1007\/3-540-45744-5_50","volume-title":"Automated Reasoning","author":"B Boigelot","year":"2001","unstructured":"Boigelot, B., Jodogne, S., Wolper, P.: On the use of weak automata for deciding linear arithmetic with integer and real variables. In: Gor\u00e9, R., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS, vol. 2083, pp. 611\u2013625. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45744-5_50"},{"key":"8_CR6","doi-asserted-by":"publisher","unstructured":"B\u00fcchi, J.R.: On a decision method in restricted second order arithmetic. In: The Collected Works of J. Richard B\u00fcchi, pp. 425\u2013435. Springer, Cham (1990). https:\/\/doi.org\/10.1007\/978-1-4613-8928-6_23","DOI":"10.1007\/978-1-4613-8928-6_23"},{"key":"8_CR7","unstructured":"Casares, A., Colcombet, T., Fijalkow, N.: Optimal transformations of games and automata using Muller conditions. In: ICALP. LIPIcs, vol. 198, pp. 123:1\u2013123:14 (2021)"},{"key":"8_CR8","doi-asserted-by":"publisher","unstructured":"Casares, A., Duret-Lutz, A., Meyer, K.J., Renkin, F., Sickert, S.: Practical applications of the alternating cycle decomposition. In: TACAS. LNCS, vol. 13244, pp. 99\u2013117. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_6","DOI":"10.1007\/978-3-030-99527-0_6"},{"key":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-642-02930-1_13","volume-title":"Automata, Languages and Programming","author":"T Colcombet","year":"2009","unstructured":"Colcombet, T., Zdanowski, K.: A tight lower bound for determinization of transition labeled B\u00fcchi automata. In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S., Thomas, W. (eds.) ICALP 2009. LNCS, vol. 5556, pp. 151\u2013162. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02930-1_13"},{"issue":"4","key":"8_CR10","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":"8_CR11","unstructured":"De Giacomo, G., Vardi, M.Y.: Linear temporal logic and linear dynamic logic on finite traces. In: IJCAI, pp. 854\u2013860 (2013)"},{"key":"8_CR12","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"},{"issue":"3","key":"8_CR13","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":"8_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"426","DOI":"10.1007\/978-3-662-54577-5_25","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J Esparza","year":"2017","unstructured":"Esparza, J., K\u0159et\u00ednsk\u00fd, J., Raskin, J.-F., Sickert, S.: From LTL and limit-deterministic B\u00fcchi automata to deterministic parity automata. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 426\u2013442. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_25"},{"issue":"6","key":"8_CR15","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3417995","volume":"67","author":"J Esparza","year":"2020","unstructured":"Esparza, J., K\u0159et\u00ednsk\u00fd, J., Sickert, S.: A unified translation of linear temporal logic to $$\\omega $$-automata. J. ACM 67(6), 1\u201361 (2020)","journal-title":"J. ACM"},{"key":"8_CR16","doi-asserted-by":"crossref","unstructured":"Farwer, B.: Omega-automata. In: Automata, Logics, and Infinite Games: A Guide to Current Research. LNCS, vol. 2500, pp. 3\u201320 (2001)","DOI":"10.1007\/3-540-36387-4_1"},{"key":"8_CR17","unstructured":"Fisman, D., Lustig, Y.: A modular approach for B\u00fcchi determinization. In: CONCUR. LIPIcs, vol. 42, pp. 368\u2013382 (2015)"},{"key":"8_CR18","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":"8_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1007\/978-3-030-99527-0_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"V Havlena","year":"2022","unstructured":"Havlena, V., Leng\u00e1l, O., Smahl\u00edkov\u00e1, B.: Sky is not the limit. In: Fisman, D., Rosu, G. (eds.) TACAS 2022. LNCS, vol. 13244, pp. 118\u2013136. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_7"},{"key":"8_CR20","volume-title":"Introduction to Automata Theory, Languages, and Computation","author":"JE Hopcroft","year":"2006","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":"8_CR21","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":"8_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-3-540-76336-9_7","volume-title":"Implementation and Application of Automata","author":"J Klein","year":"2007","unstructured":"Klein, J., Baier, C.: On-the-fly stuttering in the construction of deterministic $$\\omega $$-automata. In: Holub, J., \u017dd\u00e1rek, J. (eds.) CIAA 2007. LNCS, vol. 4783, pp. 51\u201361. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-76336-9_7"},{"key":"8_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1007\/978-3-030-01090-4_34","volume-title":"Automated Technology for Verification and Analysis","author":"J K\u0159et\u00ednsk\u00fd","year":"2018","unstructured":"K\u0159et\u00ednsk\u00fd, J., Meggendorfer, T., Sickert, S.: Owl: a library for $$\\omega $$-words, automata, and LTL. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 543\u2013550. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4_34"},{"issue":"3","key":"8_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. Log. 2(3), 408\u2013429 (2001)","journal-title":"ACM Trans. Comput. Log."},{"key":"8_CR25","doi-asserted-by":"publisher","unstructured":"Li, Y., Turrini, A., Feng, W., Vardi, M.V., Zhang, L.: Artifact for \u201cDivide-and-conquer determinization of B\u00fcchi automata based on SCC decomposition\u201d (2022). https:\/\/doi.org\/10.5281\/zenodo.6558928","DOI":"10.5281\/zenodo.6558928"},{"issue":"16","key":"8_CR26","doi-asserted-by":"publisher","first-page":"941","DOI":"10.1016\/j.ipl.2009.04.022","volume":"109","author":"W Liu","year":"2009","unstructured":"Liu, W., Wang, J.: A tighter analysis of Piterman\u2019s B\u00fcchi determinization. Inf. Process. Lett. 109(16), 941\u2013945 (2009)","journal-title":"Inf. Process. Lett."},{"key":"8_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/3-540-46691-6_8","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"C L\u00f6ding","year":"1999","unstructured":"L\u00f6ding, C.: Optimal bounds for transformations of $$\\omega $$-automata. In: Rangan, C.P., Raman, V., Ramanujam, R. (eds.) FSTTCS 1999. LNCS, vol. 1738, pp. 97\u2013109. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-46691-6_8"},{"key":"8_CR28","unstructured":"L\u00f6ding, C., Pirogov, A.: Determinization of B\u00fcchi automata: unifying the approaches of Safra and Muller-Schupp. In: ICALP. LIPIcs, vol. 132, pp. 120:1\u2013120:13 (2019)"},{"key":"8_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/978-3-030-31784-3_18","volume-title":"Automated Technology for Verification and Analysis","author":"C L\u00f6ding","year":"2019","unstructured":"L\u00f6ding, C., Pirogov, A.: New optimizations and heuristics for determinization of B\u00fcchi automata. In: Chen, Y.-F., Cheng, C.-H., Esparza, J. (eds.) ATVA 2019. LNCS, vol. 11781, pp. 317\u2013333. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-31784-3_18"},{"key":"8_CR30","unstructured":"Michel, M.: Complementation is more difficult with automata on infinite words. Technical report, CNET, Paris (Manuscript) (1988)"},{"issue":"3","key":"8_CR31","doi-asserted-by":"crossref","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."},{"issue":"2","key":"8_CR32","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1016\/0304-3975(92)90076-R","volume":"97","author":"DE Muller","year":"1992","unstructured":"Muller, D.E., Saoudi, A., Schupp, P.E.: Alternating automata, the weak monadic theory of trees and its complexity. Theor. Comput. Sci. 97(2), 233\u2013244 (1992)","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"8_CR33","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-3(3:5)2007","volume":"3","author":"N Piterman","year":"2007","unstructured":"Piterman, N.: From nondeterministic B\u00fcchi and Streett automata to deterministic parity automata. Log. Methods Comput. Sci. 3(3), 1\u201321 (2007)","journal-title":"Log. Methods Comput. Sci."},{"key":"8_CR34","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL, pp. 179\u2013190 (1989)","DOI":"10.1145\/75277.75293"},{"issue":"3\u20134","key":"8_CR35","doi-asserted-by":"publisher","first-page":"393","DOI":"10.3233\/FI-2012-744","volume":"119","author":"RR Redziejowski","year":"2012","unstructured":"Redziejowski, R.R.: An improved construction of deterministic omega-automaton using derivatives. Fundam. Informaticae 119(3\u20134), 393\u2013406 (2012)","journal-title":"Fundam. Informaticae"},{"key":"8_CR36","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":"8_CR37","doi-asserted-by":"crossref","unstructured":"Safra, S., Vardi, M.Y.: On omega-automata and temporal logic (preliminary report). In: STOC, pp. 127\u2013137 (1989)","DOI":"10.1145\/73007.73019"},{"key":"8_CR38","unstructured":"Schewe, S.: B\u00fcchi complementation made tight. In: STACS. LIPIcs, vol. 3, pp. 661\u2013672 (2009)"},{"key":"8_CR39","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"},{"issue":"4","key":"8_CR40","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-10(4:13)2014","volume":"10","author":"M Tsai","year":"2014","unstructured":"Tsai, M., Fogarty, S., Vardi, M., Tsay, Y.: State of B\u00fcchi complementation. Log. Methods Comput. Sci. 10(4), 1\u201327 (2014)","journal-title":"Log. Methods Comput. Sci."},{"key":"8_CR41","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: The rise and fall of linear temporal logic. In: GandALF (2011). Invited talk","DOI":"10.4204\/EPTCS.54.0.2"},{"issue":"1","key":"8_CR42","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"MY Vardi","year":"1994","unstructured":"Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Inf. Comput. 115(1), 1\u201337 (1994)","journal-title":"Inf. Comput."},{"key":"8_CR43","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), 1\u201320 (2008)","DOI":"10.2168\/LMCS-4(1:5)2008"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-13188-2_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,5]],"date-time":"2022-08-05T21:02:54Z","timestamp":1659733374000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-13188-2_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031131875","9783031131882"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-13188-2_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"6 August 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Haifa","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Israel","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 August 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 August 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"34","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2022\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","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":"209","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":"40","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":"11","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":"19% - 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":"3.9","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":"9.7","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)"}}]}}