{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T05:02:59Z","timestamp":1743138179600,"version":"3.40.3"},"publisher-location":"Cham","reference-count":43,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030720155"},{"type":"electronic","value":"9783030720162"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,3,20]],"date-time":"2021-03-20T00:00:00Z","timestamp":1616198400000},"content-version":"vor","delay-in-days":78,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>It is well-known that the winning region of a parity game with <jats:italic>n<\/jats:italic> nodes and <jats:italic>k<\/jats:italic> priorities can be computed as a <jats:italic>k<\/jats:italic>-nested fixpoint of a suitable function; straightforward computation of this nested fixpoint requires <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mathcal {O}(n^{\\frac{k}{2}})$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                    <mml:mrow>\n                      <mml:mi>O<\/mml:mi>\n                      <mml:mo>(<\/mml:mo>\n                      <mml:msup>\n                        <mml:mi>n<\/mml:mi>\n                        <mml:mfrac>\n                          <mml:mi>k<\/mml:mi>\n                          <mml:mn>2<\/mml:mn>\n                        <\/mml:mfrac>\n                      <\/mml:msup>\n                      <mml:mo>)<\/mml:mo>\n                    <\/mml:mrow>\n                  <\/mml:math><\/jats:alternatives><\/jats:inline-formula> iterations of the function. Calude et al.\u2019s recent quasipolynomial-time parity game solving algorithm essentially shows how to compute the same fixpoint in only quasipolynomially many iterations by reducing parity games to quasipolynomially sized safety games. Universal graphs have been used to modularize this transformation of parity games to equivalent safety games that are obtained by combining the original game with a universal graph. We show that this approach naturally generalizes to the computation of solutions of systems of <jats:italic>any<\/jats:italic> fixpoint equations over finite lattices; hence, the solution of fixpoint equation systems can be computed by quasipolynomially many iterations of the equations. We present applications to modal fixpoint logics and games beyond relational semantics. For instance, the model checking problems for the energy <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mu $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                    <mml:mi>\u03bc<\/mml:mi>\n                  <\/mml:math><\/jats:alternatives><\/jats:inline-formula>-calculus, finite latticed <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mu $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                    <mml:mi>\u03bc<\/mml:mi>\n                  <\/mml:math><\/jats:alternatives><\/jats:inline-formula>-calculi, and the graded and the (two-valued) probabilistic <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mu $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                    <mml:mi>\u03bc<\/mml:mi>\n                  <\/mml:math><\/jats:alternatives><\/jats:inline-formula>-calculus \u2013 with numbers coded in binary \u2013 can be solved via nested fixpoints of functions that differ substantially from the function for parity games but still can be computed in quasipolynomial time; our result hence implies that model checking for these <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mu $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                    <mml:mi>\u03bc<\/mml:mi>\n                  <\/mml:math><\/jats:alternatives><\/jats:inline-formula>-calculi is in <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsc {QP}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                    <mml:mrow>\n                      <mml:mi>QP<\/mml:mi>\n                      <mml:mstyle\/>\n                    <\/mml:mrow>\n                  <\/mml:math><\/jats:alternatives><\/jats:inline-formula>. Moreover, we improve the exponent in known exponential bounds on satisfiability checking.<\/jats:p>","DOI":"10.1007\/978-3-030-72016-2_3","type":"book-chapter","created":{"date-parts":[[2021,3,19]],"date-time":"2021-03-19T22:03:37Z","timestamp":1616191417000},"page":"38-56","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Quasipolynomial Computation of Nested Fixpoints"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0935-8602","authenticated-orcid":false,"given":"Daniel","family":"Hausmann","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3146-5906","authenticated-orcid":false,"given":"Lutz","family":"Schr\u00f6der","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,3,20]]},"reference":[{"key":"3_CR1","doi-asserted-by":"publisher","unstructured":"Alur, R., Henzinger, T., Kupferman, O.: Alternating-time temporal logic. J. ACM 49, 672\u2013713 (2002), https:\/\/doi.org\/10.1145\/585265.585270","DOI":"10.1145\/585265.585270"},{"key":"3_CR2","unstructured":"Amram, G., Maoz, S., Pistiner, O., Ringert, J.O.: Energy mu-calculus: Symbolic fixed-point algorithms for omega-regular energy games. CoRR abs\/2005.00641 (2020), https:\/\/arxiv.org\/abs\/2005.00641"},{"key":"3_CR3","doi-asserted-by":"publisher","unstructured":"Arnold, A., Niwinski, D., Parys, P.: A quasi-polynomial black-box algorithm for fixed point evaluation. In: Computer Science Logic, CSL 2021. LIPIcs, vol.\u00a0183, pp. 9:1\u20139:23. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik (2021), https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2021.9","DOI":"10.4230\/LIPIcs.CSL.2021.9"},{"key":"3_CR4","doi-asserted-by":"publisher","unstructured":"Baldan, P., K\u00f6nig, B., Mika-Michalski, C., Padoan, T.: Fixpoint games on continuous lattices. In: Principles of Programming Languages, POPL 2021. Proceedings of the ACM on Programming Languages, vol.\u00a03, pp. 26:1\u201326:29. ACM (2019), https:\/\/doi.org\/10.1145\/3290339","DOI":"10.1145\/3290339"},{"key":"3_CR5","doi-asserted-by":"publisher","unstructured":"Bodlaender, H., Dinneen, M., Khoussainov, B.: On game-theoretic models of networks. In: Algorithms and Computation, ISAAC 2001. LNCS, vol.\u00a02223, pp. 550\u2013561. Springer (2001), https:\/\/doi.org\/10.1007\/3-540-45678-3_47","DOI":"10.1007\/3-540-45678-3_47"},{"key":"3_CR6","doi-asserted-by":"publisher","unstructured":"Boker, U., Lehtinen, K.: On the way to alternating weak automata. In: Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2018. LIPIcs, vol.\u00a0122, pp. 21:1\u201321:22. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik (2018), https:\/\/doi.org\/10.4230\/LIPIcs.FSTTCS.2018.21","DOI":"10.4230\/LIPIcs.FSTTCS.2018.21"},{"key":"3_CR7","doi-asserted-by":"publisher","unstructured":"Bruns, G., Godefroid, P.: Model checking with multi-valued logics. In: Automata, Languages and Programming, ICALP 2004. LNCS, vol.\u00a03142, pp. 281\u2013293. Springer (2004), https:\/\/doi.org\/10.1007\/978-3-540-27836-8_26","DOI":"10.1007\/978-3-540-27836-8_26"},{"key":"3_CR8","doi-asserted-by":"publisher","unstructured":"Bruse, F., Falk, M., Lange, M.: The fixpoint-iteration algorithm for parity games. In: Games, Automata, Logics and Formal Verification, GandALF 2014. EPTCS, vol.\u00a0161, pp. 116\u2013130. Open Publishing Association (2014), https:\/\/doi.org\/10.4204\/EPTCS.161.12","DOI":"10.4204\/EPTCS.161.12"},{"key":"3_CR9","doi-asserted-by":"publisher","unstructured":"Calude, C., Jain, S., Khoussainov, B., Li, W., Stephan, F.: Deciding parity games in quasipolynomial time. In: Theory of Computing, STOC 2017. pp. 252\u2013263. ACM (2017), https:\/\/doi.org\/10.1145\/3055399.3055409","DOI":"10.1145\/3055399.3055409"},{"key":"3_CR10","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Doyen, L.: Energy parity games. Theor. Comput. Sci. 458, 49\u201360 (2012). https:\/\/doi.org\/10.1016\/j.tcs.2012.07.038","DOI":"10.1016\/j.tcs.2012.07.038"},{"key":"3_CR11","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Dvor\u00e1k, W., Henzinger, M., Svozil, A.: Quasipolynomial set-based symbolic algorithms for parity games. In: Logic for Programming, Artificial Intelligence and Reasoning, LPAR 2018. EPiC, vol.\u00a057, pp. 233\u2013253. EasyChair (2018), https:\/\/doi.org\/10.29007\/5z5k","DOI":"10.29007\/5z5k"},{"key":"3_CR12","doi-asserted-by":"publisher","unstructured":"C\u00eerstea, C., Kupke, C., Pattinson, D.: EXPTIME tableaux for the coalgebraic $$\\mu $$-calculus. Log. Meth. Comput. Sci. 7 (2011), https:\/\/doi.org\/10.2168\/LMCS-7(3:3)2011","DOI":"10.2168\/LMCS-7(3:3)2011"},{"key":"3_CR13","doi-asserted-by":"publisher","unstructured":"Colcombet, T., Fijalkow, N.: Universal graphs and good for games automata: New tools for infinite duration games. In: Foundations of Software Science and Computation Structures, FOSSACS 2019. LNCS, vol. 11425, pp. 1\u201326. Springer (2019), https:\/\/doi.org\/10.1007\/978-3-030-17127-8_1","DOI":"10.1007\/978-3-030-17127-8_1"},{"key":"3_CR14","doi-asserted-by":"publisher","unstructured":"Czerwinski, W., Daviaud, L., Fijalkow, N., Jurdzinski, M., Lazic, R., Parys, P.: Universal trees grow inside separating automata: Quasi-polynomial lower bounds for parity games. In: Symposium on Discrete Algorithms, SODA 2019. pp. 2333\u20132349. SIAM (2019), https:\/\/doi.org\/10.1137\/1.9781611975482.142","DOI":"10.1137\/1.9781611975482.142"},{"key":"3_CR15","doi-asserted-by":"publisher","unstructured":"Daviaud, L., Jurdzinski, M., Lazic, R.: A pseudo-quasi-polynomial algorithm for mean-payoff parity games. In: Logic in Computer Science, LICS 2018. pp. 325\u2013334. ACM (2018), https:\/\/doi.org\/10.1145\/3209108.3209162","DOI":"10.1145\/3209108.3209162"},{"key":"3_CR16","doi-asserted-by":"publisher","unstructured":"Dawar, A., Gr\u00e4del, E.: The descriptive complexity of parity games. In: Computer Science Logic, CSL 2008. LNCS, vol.\u00a05213, pp. 354\u2013368. Springer (2008), https:\/\/doi.org\/10.1007\/978-3-540-87531-4_26","DOI":"10.1007\/978-3-540-87531-4_26"},{"key":"3_CR17","doi-asserted-by":"publisher","unstructured":"Emerson, E.A., Jutla, C., Sistla, A.P.: On model checking for the $$\\mu $$-calculus and its fragments. Theor. Comput. Sci. 258, 491\u2013522 (2001), https:\/\/doi.org\/10.1016\/S0304-3975(00)00034-7","DOI":"10.1016\/S0304-3975(00)00034-7"},{"key":"3_CR18","doi-asserted-by":"publisher","unstructured":"Enqvist, S., Seifan, F., Venema, Y.: Monadic second-order logic and bisimulation invariance for coalgebras. In: Logic in Computer Science, LICS 2015. pp. 353\u2013365. IEEE (2015), https:\/\/doi.org\/10.1109\/LICS.2015.41","DOI":"10.1109\/LICS.2015.41"},{"key":"3_CR19","doi-asserted-by":"publisher","unstructured":"Fearnley, J., Jain, S., de\u00a0Keijzer, B., Schewe, S., Stephan, F., Wojtczak, D.: An ordered approach to solving parity games in quasi-polynomial time and quasi-linear space. STTT 21(3), 325\u2013349 (2019), https:\/\/doi.org\/10.1007\/s10009-019-00509-3","DOI":"10.1007\/s10009-019-00509-3"},{"key":"3_CR20","doi-asserted-by":"publisher","unstructured":"Friedmann, O., Lange, M.: Deciding the unguarded modal $$\\rm \\mu $$-calculus. J. Appl. Non-Classical Log. 23, 353\u2013371 (2013), https:\/\/doi.org\/10.1080\/11663081.2013.861181","DOI":"10.1080\/11663081.2013.861181"},{"key":"3_CR21","doi-asserted-by":"publisher","unstructured":"Gr\u00e4del, E., Thomas, W., Wilke, T. (eds.): Automata, Logics, and Infinite Games: A Guide to Current Research, LNCS, vol.\u00a02500. Springer (2002), https:\/\/doi.org\/10.1007\/3-540-36387-4","DOI":"10.1007\/3-540-36387-4"},{"key":"3_CR22","doi-asserted-by":"publisher","unstructured":"Hasuo, I., Shimizu, S., C\u00eerstea, C.: Lattice-theoretic progress measures and coalgebraic model checking. In: Principles of Programming Languages, POPL 2016. pp. 718\u2013732. ACM (2016), https:\/\/doi.org\/10.1145\/2837614.2837673","DOI":"10.1145\/2837614.2837673"},{"key":"3_CR23","unstructured":"Hausmann, D., Schr\u00f6der, L.: Computing nested fixpoints in quasipolynomial time. CoRR abs\/1907.07020 (2019), http:\/\/arxiv.org\/abs\/1907.07020"},{"key":"3_CR24","doi-asserted-by":"publisher","unstructured":"Hausmann, D., Schr\u00f6der, L.: Game-based local model checking for the coalgebraic $$\\mu $$-calculus. In: Concurrency Theory, CONCUR 2019. LIPIcs, vol.\u00a0140, pp. 35:1\u201335:16. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik (2019), https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2019.35","DOI":"10.4230\/LIPIcs.CONCUR.2019.35"},{"key":"3_CR25","doi-asserted-by":"publisher","unstructured":"Hausmann, D., Schr\u00f6der, L.: Optimal satisfiability checking for arithmetic $$\\mu $$-calculi. In: Foundations of Software Science and Computation Structures, FOSSACS 2019. LNCS, vol. 11425, pp. 277\u2013294. Springer (2019), https:\/\/doi.org\/10.1007\/978-3-030-17127-8_16","DOI":"10.1007\/978-3-030-17127-8_16"},{"key":"3_CR26","doi-asserted-by":"publisher","unstructured":"Henzinger, T., Rajamani, S.: Fair bisimulation. In: Tools and Algorithms for Construction and Analysis of Systems, TACAS 2000. LNCS, vol.\u00a01785, pp. 299\u2013314. Springer (2000), https:\/\/doi.org\/10.1007\/3-540-46419-0_21","DOI":"10.1007\/3-540-46419-0_21"},{"key":"3_CR27","doi-asserted-by":"publisher","unstructured":"Jurdzi\u0144ski, M.: Small progress measures for solving parity games. In: Symposium on Theoretical Aspects of Computer Science, STACS 2000. LNCS, vol.\u00a01770, pp. 290\u2013301. Springer (2000), https:\/\/doi.org\/10.1007\/3-540-46541-3_24","DOI":"10.1007\/3-540-46541-3_24"},{"key":"3_CR28","doi-asserted-by":"publisher","unstructured":"Jurdzinski, M., Lazic, R.: Succinct progress measures for solving parity games. In: Logic in Computer Science, LICS 2017. pp.\u00a01\u20139. IEEE Computer Society (2017), https:\/\/doi.org\/10.1109\/LICS.2017.8005092","DOI":"10.1109\/LICS.2017.8005092"},{"key":"3_CR29","doi-asserted-by":"publisher","unstructured":"Kozen, D.: Results on the propositional $$\\mu $$-calculus. Theor. Comput. Sci. 27, 333\u2013354 (1983), https:\/\/doi.org\/10.1016\/0304-3975(82)90125-6","DOI":"10.1016\/0304-3975(82)90125-6"},{"key":"3_CR30","doi-asserted-by":"publisher","unstructured":"Kupferman, O., Lustig, Y.: Latticed simulation relations and games. In: Automated Technology for Verification and Analysis, ATVA 2007. LNCS, vol.\u00a04762, pp. 316\u2013330. Springer (2007), https:\/\/doi.org\/10.1007\/978-3-540-75596-8_23","DOI":"10.1007\/978-3-540-75596-8_23"},{"key":"3_CR31","doi-asserted-by":"publisher","unstructured":"Kupferman, O., Piterman, N., Vardi, M.: Fair equivalence relations. In: Verification: Theory and Practice. LNCS, vol.\u00a02772, pp. 702\u2013732. Springer (2003), https:\/\/doi.org\/10.1007\/978-3-540-39910-0_30","DOI":"10.1007\/978-3-540-39910-0_30"},{"key":"3_CR32","doi-asserted-by":"publisher","unstructured":"Kupferman, O., Sattler, U., Vardi, M.: The complexity of the graded $$\\mu $$-calculus. In: Automated Deduction, CADE 2002. LNCS, vol.\u00a02392, pp. 423\u2013437. Springer (2002), https:\/\/doi.org\/10.1007\/3-540-45620-1_34","DOI":"10.1007\/3-540-45620-1_34"},{"key":"3_CR33","doi-asserted-by":"publisher","unstructured":"Lehtinen, K.: A modal $$\\mu $$ perspective on solving parity games in quasi-polynomial time. In: Logic in Computer Science, LICS 2018. pp. 639\u2013648. ACM (2018), https:\/\/doi.org\/10.1145\/3209108.3209115","DOI":"10.1145\/3209108.3209115"},{"key":"3_CR34","unstructured":"Liu, W., Song, L., Wang, J., Zhang, L.: A simple probabilistic extension of modal mu-calculus. In: International Joint Conference on Artificial Intelligence, IJCAI 2015. pp. 882\u2013888. AAAI Press (2015), http:\/\/ijcai.org\/proceedings\/2015"},{"key":"3_CR35","doi-asserted-by":"publisher","unstructured":"Long, D.E., Browne, A., Clarke, E.M., Jha, S., Marrero, W.R.: An improved algorithm for the evaluation of fixpoint expressions. In: Computer Aided Verification, CAV 1994. LNCS, vol.\u00a0818, pp. 338\u2013350. Springer (1994), https:\/\/doi.org\/10.1007\/3-540-58179-0_66","DOI":"10.1007\/3-540-58179-0_66"},{"key":"3_CR36","doi-asserted-by":"publisher","unstructured":"Mio, M.: On the equivalence of game and denotational semantics for the probabilistic $$\\mu $$-calculus. Log. Methods Comput. Sci. 8 (2012), https:\/\/doi.org\/10.2168\/LMCS-8(2:7)2012","DOI":"10.2168\/LMCS-8(2:7)2012"},{"key":"3_CR37","doi-asserted-by":"publisher","unstructured":"Parikh, R.: The logic of games and its applications. Ann. Discr. Math. 24, 111\u2013140 (1985), https:\/\/doi.org\/10.1016\/S0304-0208(08)73078-0","DOI":"10.1016\/S0304-0208(08)73078-0"},{"key":"3_CR38","doi-asserted-by":"publisher","unstructured":"Parys, P.: Parity games: Zielonka\u2019s algorithm in quasi-polynomial time. In: Mathematical Foundations of Computer Science, MFCS 2019. LIPIcs, vol.\u00a0138, pp. 10:1\u201310:13. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik (2019), https:\/\/doi.org\/10.4230\/LIPIcs.MFCS.2019.10","DOI":"10.4230\/LIPIcs.MFCS.2019.10"},{"key":"3_CR39","doi-asserted-by":"publisher","unstructured":"Peleg, D.: Concurrent dynamic logic. J. ACM 34, 450\u2013479 (1987), https:\/\/doi.org\/10.1145\/23005.23008.","DOI":"10.1145\/23005.23008"},{"key":"3_CR40","doi-asserted-by":"publisher","unstructured":"Rutten, J.: Universal coalgebra: A theory of systems. Theor. Comput. Sci. 249, 3\u201380 (2000), https:\/\/doi.org\/10.1016\/S0304-3975(00)00056-6","DOI":"10.1016\/S0304-3975(00)00056-6"},{"key":"3_CR41","doi-asserted-by":"publisher","unstructured":"Seidl, H.: Fast and Simple Nested Fixpoints. Inf. Process. Lett. 59, 303\u2013308 (1996), https:\/\/doi.org\/10.1016\/0020-0190(96)00130-5","DOI":"10.1016\/0020-0190(96)00130-5"},{"key":"3_CR42","unstructured":"Venema, Y.: Lectures on the modal $$\\mu $$-calculus. Lecture notes, Institute for Logic, Language and Computation, Universiteit van Amsterdam (2008), https:\/\/staff.fnwi.uva.nl\/y.venema\/teaching\/ml\/notes\/20201212-mu.pdf"},{"key":"3_CR43","doi-asserted-by":"publisher","unstructured":"Zielonka, W.: Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theor. Comput. Sci. 200(1-2), 135\u2013183 (1998), https:\/\/doi.org\/10.1016\/S0304-3975(98)00009-7","DOI":"10.1016\/S0304-3975(98)00009-7"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-72016-2_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T00:05:59Z","timestamp":1616371559000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-72016-2_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030720155","9783030720162"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-72016-2_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"20 March 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 March 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 April 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2021\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-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":"141","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":"41","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":"21","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":"29% - 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","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":"12","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)"}},{"value":"The conference changed to an online format due to the COVID-19 pandemic","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}