{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T08:13:47Z","timestamp":1743063227505,"version":"3.40.3"},"publisher-location":"Cham","reference-count":53,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030888848"},{"type":"electronic","value":"9783030888855"}],"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:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-88885-5_1","type":"book-chapter","created":{"date-parts":[[2021,10,13]],"date-time":"2021-10-13T17:25:06Z","timestamp":1634145906000},"page":"3-12","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Linear Temporal Logic \u2013 From Infinite to\u00a0Finite Horizon"],"prefix":"10.1007","author":[{"given":"Lucas M.","family":"Tabajara","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,10,12]]},"reference":[{"key":"1_CR1","doi-asserted-by":"crossref","unstructured":"Almagor, S., Boker, U., Kupferman, O.: Formally reasoning about quality. J. ACM 63(3), 24:1\u201324:56 (2016). https:\/\/doi.org\/10.1145\/2875421","DOI":"10.1145\/2875421"},{"key":"1_CR2","unstructured":"Almagor, S., Kupferman, O.: High-quality synthesis against stochastic environments. In: Talbot, J., Regnier, L. (eds.) CSL. LIPIcs, vol. 62, pp. 28:1\u201328:17. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2016)"},{"key":"1_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/11605157_22","volume-title":"Implementation and Application of Automata","author":"CS Althoff","year":"2006","unstructured":"Althoff, C.S., Thomas, W., Wallmeier, N.: Observations on determinization of B\u00fcchi automata. In: Farr\u00e9, J., Litovsky, I., Schmitz, S. (eds.) CIAA 2005. LNCS, vol. 3845, pp. 262\u2013272. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11605157_22"},{"key":"1_CR4","doi-asserted-by":"publisher","unstructured":"Alur, R., Torre, S.L.: Deterministic generators and games for LTL fragments. In: IEEE, pp. 291\u2013300. IEEE Computer Society (2001). https:\/\/doi.org\/10.1109\/LICS.2001.932505","DOI":"10.1109\/LICS.2001.932505"},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"Bansal, S., Li, Y., Tabajara, L.M., Vardi, M.Y.: Hybrid compositional reasoning for reactive synthesis from finite-horizon specifications. In: AAAI, pp. 9766\u20139774 (2020)","DOI":"10.1609\/aaai.v34i06.6528"},{"issue":"3","key":"1_CR6","doi-asserted-by":"publisher","first-page":"911","DOI":"10.1016\/j.jcss.2011.08.007","volume":"78","author":"R Bloem","year":"2012","unstructured":"Bloem, R., Jobstmann, B., Piterman, N., Pnueli, A., Sa\u2019ar, Y.: Synthesis of reactive(1) designs. J. Comput. Syst. Sci. 78(3), 911\u2013938 (2012)","journal-title":"J. Comput. Syst. Sci."},{"key":"1_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"652","DOI":"10.1007\/978-3-642-31424-7_45","volume-title":"Computer Aided Verification","author":"A Bohy","year":"2012","unstructured":"Bohy, A., Bruy\u00e8re, V., Filiot, E., Jin, N., Raskin, J.-F.: Acacia+, a tool for LTL synthesis. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 652\u2013657. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_45"},{"key":"1_CR8","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1007\/978-1-4613-8928-6_22","volume-title":"The Collected Works of J. Richard B\u00fcchi","author":"JR B\u00fcchi","year":"1990","unstructured":"B\u00fcchi, J.R.: Weak second-order arithmetic and finite automata. In: Mac, L.S., Siefkes, D. (eds.) The Collected Works of J. Richard B\u00fcchi, pp. 398\u2013424. Springer, New York (1990). https:\/\/doi.org\/10.1007\/978-1-4613-8928-6_22"},{"key":"1_CR9","doi-asserted-by":"crossref","unstructured":"Calude, C.S., Jain, S., Khoussainov, B., Li, W., Stephan, F.: Deciding parity games in quasipolynomial time. In: STOC, pp. 252\u2013263 (2017)","DOI":"10.1145\/3055399.3055409"},{"key":"1_CR10","doi-asserted-by":"crossref","unstructured":"Camacho, A., Baier, J.A., Muise, C.J., McIlraith, S.A.: Finite LTL synthesis as planning. In: ICAPS, pp. 29\u201338 (2018)","DOI":"10.24963\/ijcai.2018\/848"},{"key":"1_CR11","doi-asserted-by":"crossref","unstructured":"Camacho, A., Triantafillou, E., Muise, C., Baier, J.A., McIlraith, S.: Non-deterministic planning with temporally extended goals: LTL over finite and infinite traces. In: AAAI, pp. 3716\u20133724 (2017)","DOI":"10.1609\/aaai.v31i1.11058"},{"key":"1_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/978-3-319-41528-4_6","volume-title":"Computer Aided Verification","author":"C-H Cheng","year":"2016","unstructured":"Cheng, C.-H., Hamza, Y., Ruess, H.: Structural synthesis for GXW specifications. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 95\u2013117. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_6"},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"De Giacomo, G., Di Stasio, A., Tabajara, L.M., Vardi, M., Zhu, S.: Finite-trace and generalized-reactivity specifications in temporal synthesis. In: IJCAI (2021)","DOI":"10.24963\/ijcai.2021\/255"},{"key":"1_CR14","doi-asserted-by":"crossref","unstructured":"De Giacomo, G., Di Stasio, A., Vardi, M.Y., Zhu, S.: Two-stage technique for LTL$$_f$$ synthesis under LTL assumptions. In: KR (2020)","DOI":"10.24963\/kr.2020\/31"},{"key":"1_CR15","doi-asserted-by":"crossref","unstructured":"De Giacomo, G., Rubin, S.: Automata-theoretic foundations of FOND planning for LTL$$_f$$\/LDL$$_f$$ Goals. In: IJCAI, pp. 4729\u20134735 (2018)","DOI":"10.24963\/ijcai.2018\/657"},{"key":"1_CR16","unstructured":"De Giacomo, G., Vardi, M.Y.: Linear temporal logic and linear dynamic logic on finite traces. In: IJCAI, pp. 854\u2013860 (2013)"},{"key":"1_CR17","unstructured":"De Giacomo, G., Vardi, M.Y.: Synthesis for LTL and LDL on finite traces. In: IJCAI, pp. 1558\u20131564 (2015)"},{"key":"1_CR18","unstructured":"De Giacomo, G., Vardi, M.Y.: LTL$$_f$$ and LDL$$_f$$ synthesis under partial observability. In: IJCAI, pp. 1044\u20131050 (2016)"},{"key":"1_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/978-3-642-19835-9_25","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Ehlers","year":"2011","unstructured":"Ehlers, R.: Unbeast: symbolic bounded synthesis. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 272\u2013275. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19835-9_25"},{"key":"1_CR20","doi-asserted-by":"crossref","unstructured":"Emerson, E., Jutla, C.: On simultaneously determinizing and complementing $$\\omega $$-automata. In: Proceedings of 4th IEEE Symposium on Logic in Computer Science, pp. 333\u2013342 (1989)","DOI":"10.1109\/LICS.1989.39188"},{"key":"1_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/978-3-662-54577-5_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P Faymonville","year":"2017","unstructured":"Faymonville, P., Finkbeiner, B., Rabe, M.N., Tentrup, L.: Encodings of bounded synthesis. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 354\u2013370. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_20"},{"key":"1_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/978-3-319-63390-9_17","volume-title":"Computer Aided Verification","author":"P Faymonville","year":"2017","unstructured":"Faymonville, P., Finkbeiner, B., Tentrup, L.: BoSy: an experimentation framework for bounded synthesis. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 325\u2013332. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_17"},{"issue":"5\u20136","key":"1_CR23","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/s10009-012-0228-z","volume":"15","author":"B Finkbeiner","year":"2013","unstructured":"Finkbeiner, B., Schewe, S.: Bounded synthesis. Int. J. Softw. Tools Technol. Transf. 15(5\u20136), 519\u2013539 (2013). https:\/\/doi.org\/10.1007\/s10009-012-0228-z","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"1_CR24","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: A Guide to Current Research [outcome of a Dagstuhl seminar, February 2001]","year":"2002","unstructured":"Gr\u00e4del, E., Thomas, W., Wilke, T. (eds.): Automata, Logics, and Infinite Games: A Guide to Current Research [outcome of a Dagstuhl seminar, February 2001]. Lecture Notes in Computer Science, vol. 2500. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-36387-4"},{"key":"1_CR25","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1007\/978-3-642-82453-1_17","volume-title":"Logics and Models of Concurrent Systems, NATO Advanced Summer Institutes","author":"D Harel","year":"1985","unstructured":"Harel, D., Pnueli, A.: On the development of reactive systems. In: Apt, K. (ed.) Logics and Models of Concurrent Systems, NATO Advanced Summer Institutes, vol. 13, pp. 477\u2013498. Springer, Heidelberg (1985). https:\/\/doi.org\/10.1007\/978-3-642-82453-1_17"},{"key":"1_CR26","doi-asserted-by":"crossref","unstructured":"He, K., Wells, A.M., Kavraki, L.E., Vardi, M.Y.: Efficient symbolic reactive synthesis for finite-horizon tasks. In: ICRA, pp. 8993\u20138999. IEEE (2019)","DOI":"10.1109\/ICRA.2019.8794170"},{"key":"1_CR27","doi-asserted-by":"crossref","unstructured":"Henriksen, J.G., et al.: MONA: monadic second-order logic in practice. In: TACAS, pp. 89\u2013110 (1995)","DOI":"10.1007\/3-540-60630-0_5"},{"key":"1_CR28","doi-asserted-by":"crossref","unstructured":"Hopcroft, J.: An $$n\\log n$$ algorithm for minimizing states in a finite automaton. In: Theory of machines and computations, pp. 189\u2013196. Elsevier (1971)","DOI":"10.1016\/B978-0-12-417750-5.50022-1"},{"issue":"6","key":"1_CR29","doi-asserted-by":"publisher","first-page":"1370","DOI":"10.1109\/TRO.2009.2030225","volume":"25","author":"H Kress-Gazit","year":"2009","unstructured":"Kress-Gazit, H., Fainekos, G.E., Pappas, G.J.: Temporal-logic-based reactive mission and motion planning. IEEE Trans. Rob. 25(6), 1370\u20131381 (2009)","journal-title":"IEEE Trans. Rob."},{"key":"1_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/3-540-58325-4_202","volume-title":"Algorithms and Computation","author":"SC Krishnan","year":"1994","unstructured":"Krishnan, S.C., Puri, A., Brayton, R.K.: Deterministic $$\\omega $$ automata vis-a-vis deterministic Buchi automata. In: Du, D.-Z., Zhang, X.-S. (eds.) ISAAC 1994. LNCS, vol. 834, pp. 378\u2013386. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-58325-4_202"},{"key":"1_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/978-3-642-27660-6_8","volume-title":"SOFSEM 2012: Theory and Practice of Computer Science","author":"O Kupferman","year":"2012","unstructured":"Kupferman, O.: Recent challenges and ideas in temporal synthesis. In: Bielikov\u00e1, M., Friedrich, G., Gottlob, G., Katzenbeisser, S., Tur\u00e1n, G. (eds.) SOFSEM 2012. LNCS, vol. 7147, pp. 88\u201398. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-27660-6_8"},{"key":"1_CR32","unstructured":"Kupferman, O., Vardi, M.: Synthesis with incomplete informatio. In: ICTL, pp. 1044\u20131050 (1997)"},{"issue":"3","key":"1_CR33","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1109\/TRO.2016.2544339","volume":"32","author":"M Lahijanian","year":"2016","unstructured":"Lahijanian, M., Maly, M.R., Fried, D., Kavraki, L.E., Kress-Gazit, H., Vardi, M.Y.: Iterative temporal planning in uncertain environments with partial satisfaction guarantees. IEEE Trans. Robot. 32(3), 583\u2013599 (2016)","journal-title":"IEEE Trans. Robot."},{"key":"1_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/3-540-36387-4_2","volume-title":"Automata Logics, and Infinite Games","author":"R Mazala","year":"2002","unstructured":"Mazala, R.: Infinite games. In: Gr\u00e4del, E., Thomas, W., Wilke, T. (eds.) Automata Logics, and Infinite Games. LNCS, vol. 2500, pp. 23\u201338. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-36387-4_2"},{"key":"1_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"578","DOI":"10.1007\/978-3-319-96145-3_31","volume-title":"Computer Aided Verification","author":"PJ Meyer","year":"2018","unstructured":"Meyer, P.J., Sickert, S., Luttenberger, M.: Strix: explicit reactive synthesis strikes back! In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 578\u2013586. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_31"},{"issue":"3\u20134","key":"1_CR36","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/s10514-019-09861-4","volume":"44","author":"S Moarref","year":"2020","unstructured":"Moarref, S., Kress-Gazit, H.: Automated synthesis of decentralized controllers for robot swarms from high-level temporal logic specifications. Auton. Robot. 44(3\u20134), 585\u2013600 (2020). https:\/\/doi.org\/10.1007\/s10514-019-09861-4","journal-title":"Auton. Robot."},{"key":"1_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-642-16164-3_11","volume-title":"Model Checking Software","author":"M Pe\u0161i\u0107","year":"2010","unstructured":"Pe\u0161i\u0107, M., Bo\u0161na\u010dki, D., van der Aalst, W.M.P.: Enacting declarative languages using LTL: avoiding errors and improving performance. In: van de Pol, J., Weber, M. (eds.) SPIN 2010. LNCS, vol. 6349, pp. 146\u2013161. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-16164-3_11"},{"key":"1_CR38","doi-asserted-by":"crossref","unstructured":"Piterman, N.: From nondeterministic B\u00fcchi and streett automata to deterministic parity automata. Log. Methods Comput. Sci. 3(3) (2007)","DOI":"10.2168\/LMCS-3(3:5)2007"},{"key":"1_CR39","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"1_CR40","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"},{"key":"1_CR41","unstructured":"Rosner, R.: Modular synthesis of reactive systems. Ph.D. thesis, The Weizmann Institute of Science (1991)"},{"key":"1_CR42","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"},{"issue":"3","key":"1_CR43","doi-asserted-by":"publisher","first-page":"803","DOI":"10.1137\/S0097539798332518","volume":"36","author":"S Safra","year":"2006","unstructured":"Safra, S.: Exponential determinization for $$\\omega $$-automata with a strong fairness acceptance condition. SIAM J. Comput. 36(3), 803\u2013814 (2006)","journal-title":"SIAM J. Comput."},{"key":"1_CR44","unstructured":"Schewe, S.: Beyond hyper-minimisation\u2013minimising DBAs and DPAs is NP-complete. In: Proceedings of IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. LIPIcs, vol. 8, pp. 400\u2013411. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2010)"},{"key":"1_CR45","doi-asserted-by":"publisher","unstructured":"Tabajara, L.M., Vardi, M.Y.: LTL$$_f$$ synthesis under partial observability: from theory to practice. In: Raskin, J., Bresolin, D. (eds.) GandALF. EPTCS, vol. 326, pp. 1\u201317 (2020). https:\/\/doi.org\/10.4204\/EPTCS.326.1","DOI":"10.4204\/EPTCS.326.1"},{"key":"1_CR46","doi-asserted-by":"crossref","unstructured":"Tabajara, L.M., Vardi, M.Y.: Partitioning techniques in LTL$$_f$$ synthesis. In: IJCAI, pp. 5599\u20135606. AAAI Press (2019)","DOI":"10.24963\/ijcai.2019\/777"},{"key":"1_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/3-540-60385-9_16","volume-title":"Correct Hardware Design and Verification Methods","author":"S Ta\u015eiran","year":"1995","unstructured":"Ta\u015eiran, S., Hojati, R., Brayton, R.K.: Language containment of non-deterministic $$\\omega $$-automata. In: Camurati, P.E., Eveking, H. (eds.) CHARME 1995. LNCS, vol. 987, pp. 261\u2013277. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/3-540-60385-9_16"},{"key":"1_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/978-3-540-69738-1_10","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"MY Vardi","year":"2007","unstructured":"Vardi, M.Y.: Automata-theoretic model checking revisited. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 137\u2013150. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-69738-1_10"},{"key":"1_CR49","doi-asserted-by":"crossref","unstructured":"Wells, A.M., Lahijanian, M., Kavraki, L.E., Vardi, M.Y.: LTL$$_f$$ synthesis on probabilistic systems. In: Raskin, J., Bresolin, D. (eds.) GandALF. EPTCS, vol. 326, pp. 166\u2013181 (2020). https:\/\/doi.org\/10.4204\/EPTCS.326.11","DOI":"10.4204\/EPTCS.326.11"},{"key":"1_CR50","doi-asserted-by":"crossref","unstructured":"Zhu, S., De Giacomo, G., Pu, G., Vardi, M.Y.: LTL$$_f$$ synthesis with fairness and stability assumptions. In: AAAI, pp. 3088\u20133095 (2020)","DOI":"10.1609\/aaai.v34i03.5704"},{"key":"1_CR51","doi-asserted-by":"crossref","unstructured":"Zhu, S., Pu, G., Vardi, M.Y.: First-order vs. second-order encodings for LTL$$_f$$-to-automata translation. In: TAMC, pp. 684\u2013705 (2019)","DOI":"10.1007\/978-3-030-14812-6_43"},{"key":"1_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-319-70389-3_10","volume-title":"Hardware and Software: Verification and Testing","author":"S Zhu","year":"2017","unstructured":"Zhu, S., Tabajara, L.M., Li, J., Pu, G., Vardi, M.Y.: A symbolic approach to safety LTL synthesis. In: HVC 2017. LNCS, vol. 10629, pp. 147\u2013162. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-70389-3_10"},{"key":"1_CR53","doi-asserted-by":"crossref","unstructured":"Zhu, S., Tabajara, L.M., Li, J., Pu, G., Vardi, M.Y.: Symbolic LTL$$_f$$ synthesis. In: IJCAI, pp. 1362\u20131369 (2017)","DOI":"10.24963\/ijcai.2017\/189"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-88885-5_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T22:16:40Z","timestamp":1725920200000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-88885-5_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030888848","9783030888855"],"references-count":53,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-88885-5_1","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":"12 October 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ATVA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Automated Technology for Verification and Analysis","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Gold Coast, QLD","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Australia","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":"18 October 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 October 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"atva2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/formal-analysis.com\/atva\/2021\/","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":"75","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":"19","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":"25% - 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":"3","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":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"In addition there are 4 tool papers. The conference was held online because of 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)"}}]}}