{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T20:13:14Z","timestamp":1784837594867,"version":"3.55.0"},"publisher-location":"Cham","reference-count":53,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030720155","type":"print"},{"value":"9783030720162","type":"electronic"}],"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>This paper presents an efficient procedure for multi-objective model checking of long-run average reward (aka: mean pay-off) and total reward objectives as well as their combination. We consider this for Markov automata, a compositional model that captures both traditional Markov decision processes (MDPs) as well as a continuous-time variant thereof. The crux of our procedure is a generalization of Forejt <jats:italic>et al.<\/jats:italic>\u2019s approach for total rewards on MDPs to arbitrary combinations of long-run and total reward objectives on Markov automata. Experiments with a prototypical implementation on top of the <jats:sc>Storm<\/jats:sc> model checker show encouraging results for both model types and indicate a substantial improved performance over existing multi-objective long-run MDP model checking based on linear programming.<\/jats:p>","DOI":"10.1007\/978-3-030-72016-2_13","type":"book-chapter","created":{"date-parts":[[2021,3,19]],"date-time":"2021-03-19T22:03:37Z","timestamp":1616191417000},"page":"230-249","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Multi-objective Optimization of Long-run Average and Total Rewards"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2843-5511","authenticated-orcid":false,"given":"Tim","family":"Quatmann","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6143-1926","authenticated-orcid":false,"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2021,3,20]]},"reference":[{"key":"13_CR1","doi-asserted-by":"publisher","unstructured":"Ashok, P., Chatterjee, K., Daca, P., Kret\u00ednsk\u00fd, J., Meggendorfer, T.: Value iteration for long-run average reward in Markov decision processes. In: CAV (1). LNCS, vol. 10426, pp. 201\u2013221. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_10","DOI":"10.1007\/978-3-319-63387-9_10"},{"key":"13_CR2","doi-asserted-by":"publisher","unstructured":"Ashok, P., Chatterjee, K., Kret\u00ednsk\u00fd, J., Weininger, M., Winkler, T.: Approximating values of generalized-reachability stochastic games. In: LICS. pp. 102\u2013115. ACM (2020). https:\/\/doi.org\/10.1145\/3373718.3394761","DOI":"10.1145\/3373718.3394761"},{"key":"13_CR3","doi-asserted-by":"publisher","unstructured":"Baier, C., Bertrand, N., Dubslaff, C., Gburek, D., Sankur, O.: Stochastic shortest paths and weight-bounded properties in Markov decision processes. In: LICS. pp. 86\u201394. ACM (2018). https:\/\/doi.org\/10.1145\/3209108.3209184","DOI":"10.1145\/3209108.3209184"},{"key":"13_CR4","doi-asserted-by":"publisher","unstructured":"Baier, C., Dubslaff, C., Kl\u00fcppelholz, S.: Trade-off analysis meets probabilistic model checking. In: CSL-LICS. pp. 1:1\u20131:10. ACM (2014). https:\/\/doi.org\/10.1145\/2603088.2603089","DOI":"10.1145\/2603088.2603089"},{"key":"13_CR5","doi-asserted-by":"publisher","unstructured":"Baier, C., Dubslaff, C., Kl\u00fcppelholz, S., Daum, M., Klein, J., M\u00e4rcker, S., Wunderlich, S.: Probabilistic model checking and non-standard multi-objective reasoning. In: Gnesi, S., Rensink, A. (eds.) FASE. LNCS, vol. 8411, pp. 1\u201316. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-642-54804-8_1","DOI":"10.1007\/978-3-642-54804-8_1"},{"key":"13_CR6","doi-asserted-by":"publisher","unstructured":"Baier, C., Dubslaff, C., Korenciak, L., Kucera, A., Reh\u00e1k, V.: Synthesis of optimal resilient control strategies. In: ATVA. LNCS, vol. 10482, pp. 417\u2013434. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-68167-2_27","DOI":"10.1007\/978-3-319-68167-2_27"},{"key":"13_CR7","doi-asserted-by":"publisher","unstructured":"Baier, C., Hermanns, H., Katoen, J.: The 10, 000 facets of MDP model checking. In: Computing and Software Science, LNCS, vol. 10000, pp. 420\u2013451. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-319-91908-9_21","DOI":"10.1007\/978-3-319-91908-9_21"},{"key":"13_CR8","doi-asserted-by":"publisher","unstructured":"Basset, N., Kwiatkowska, M.Z., Topcu, U., Wiltsche, C.: Strategy synthesis for stochastic games with multiple long-run objectives. In: TACAS. LNCS, vol. 9035, pp. 256\u2013271. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_22","DOI":"10.1007\/978-3-662-46681-0_22"},{"key":"13_CR9","doi-asserted-by":"publisher","unstructured":"Basset, N., Kwiatkowska, M.Z., Wiltsche, C.: Compositional strategy synthesis for stochastic games with multiple objectives. Inf. Comput. 261(Part), 536\u2013587 (2018). https:\/\/doi.org\/10.1016\/j.ic.2017.09.010","DOI":"10.1016\/j.ic.2017.09.010"},{"key":"13_CR10","doi-asserted-by":"publisher","unstructured":"Bork, A., Junges, S., Katoen, J., Quatmann, T.: Verification of indefinite-horizon POMDPs. In: ATVA. LNCS, vol. 12302, pp. 288\u2013304. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-59152-6_16","DOI":"10.1007\/978-3-030-59152-6_16"},{"key":"13_CR11","doi-asserted-by":"publisher","unstructured":"Br\u00e1zdil, T., Brozek, V., Chatterjee, K., Forejt, V., Kucera, A.: Two views on multiple mean-payoff objectives in Markov decision processes. LMCS 10(1) (2014). https:\/\/doi.org\/10.2168\/LMCS-10(1:13)2014","DOI":"10.2168\/LMCS-10(1:13)2014"},{"key":"13_CR12","doi-asserted-by":"publisher","unstructured":"Br\u00e1zdil, T., Chatterjee, K., Forejt, V., Kucera, A.: MultiGain: A controller synthesis tool for MDPs with multiple mean-payoff objectives. In: TACAS. LNCS, vol. 9035, pp. 181\u2013187. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_12","DOI":"10.1007\/978-3-662-46681-0_12"},{"key":"13_CR13","doi-asserted-by":"publisher","unstructured":"Br\u00e1zdil, T., Chatterjee, K., Forejt, V., Kucera, A.: Trading performance for stability in Markov decision processes. J. Comput. Syst. Sci. 84, 144\u2013170 (2017). https:\/\/doi.org\/10.1016\/j.jcss.2016.09.009","DOI":"10.1016\/j.jcss.2016.09.009"},{"key":"13_CR14","doi-asserted-by":"publisher","unstructured":"Budde, C.E., Dehnert, C., Hahn, E.M., Hartmanns, A., Junges, S., Turrini, A.: JANI: quantitative model and tool interaction. In: TACAS (2). LNCS, vol. 10206, pp. 151\u2013168 (2017). https:\/\/doi.org\/10.1007\/978-3-662-54580-5_9","DOI":"10.1007\/978-3-662-54580-5_9"},{"key":"13_CR15","doi-asserted-by":"publisher","unstructured":"Butkova, Y., Fox, G.: Optimal time-bounded reachability analysis for concurrent systems. In: TACAS (2). LNCS, vol. 11428, pp. 191\u2013208. Springer (2019), https:\/\/doi.org\/10.1007\/978-3-030-17465-1_11","DOI":"10.1007\/978-3-030-17465-1_11"},{"key":"13_CR16","doi-asserted-by":"publisher","unstructured":"Butkova, Y., Hatefi, H., Hermanns, H., Krc\u00e1l, J.: Optimal continuous time Markov decisions. In: ATVA. LNCS, vol. 9364, pp. 166\u2013182. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-24953-7_12","DOI":"10.1007\/978-3-319-24953-7_12"},{"key":"13_CR17","doi-asserted-by":"publisher","unstructured":"Butkova, Y., Wimmer, R., Hermanns, H.: Long-run rewards for Markov automata. In: TACAS (2). LNCS, vol. 10206, pp. 188\u2013203 (2017). https:\/\/doi.org\/10.1007\/978-3-662-54580-5_11","DOI":"10.1007\/978-3-662-54580-5_11"},{"key":"13_CR18","doi-asserted-by":"publisher","unstructured":"Chatterjee, K.: Markov decision processes with multiple long-run average objectives. In: FSTTCS. LNCS, vol. 4855, pp. 473\u2013484. Springer (2007). https:\/\/doi.org\/10.1007\/978-3-540-77050-3_39","DOI":"10.1007\/978-3-540-77050-3_39"},{"key":"13_CR19","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Doyen, L.: Perfect-information stochastic games with generalized mean-payoff objectives. In: LICS. pp. 247\u2013256. ACM (2016). https:\/\/doi.org\/10.1145\/2933575.2934513","DOI":"10.1145\/2933575.2934513"},{"key":"13_CR20","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Kret\u00ednsk\u00e1, Z., Kret\u00ednsk\u00fd, J.: Unifying two views on multiple mean-payoff objectives in Markov decision processes. LMCS 13(2) (2017). https:\/\/doi.org\/10.23638\/LMCS-13(2:15)2017","DOI":"10.23638\/LMCS-13(2:15)2017"},{"key":"13_CR21","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Majumdar, R., Henzinger, T.A.: Markov decision processes with multiple objectives. In: STACS. LNCS, vol. 3884, pp. 325\u2013336. Springer (2006), https:\/\/doi.org\/10.1007\/11672142_26","DOI":"10.1007\/11672142_26"},{"key":"13_CR22","doi-asserted-by":"publisher","unstructured":"Delgrange, F., Katoen, J., Quatmann, T., Randour, M.: Simple strategies in multi-objective MDPs. In: TACAS (1). LNCS, vol. 12078, pp. 346\u2013364. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-45190-5_19","DOI":"10.1007\/978-3-030-45190-5_19"},{"key":"13_CR23","doi-asserted-by":"publisher","unstructured":"Deng, Y., Hennessy, M.: On the semantics of Markov automata. Inf. Comput. 222, 139\u2013168 (2013). https:\/\/doi.org\/10.1016\/j.ic.2012.10.010.","DOI":"10.1016\/j.ic.2012.10.010"},{"key":"13_CR24","doi-asserted-by":"crossref","unstructured":"Eisentraut, C., Hermanns, H., Katoen, J., Zhang, L.: A semantics for every GSPN. In: Petri Nets. LNCS, vol. 7927, pp. 90\u2013109. Springer (2013)","DOI":"10.1007\/978-3-642-38697-8_6"},{"key":"13_CR25","doi-asserted-by":"publisher","unstructured":"Eisentraut, C., Hermanns, H., Zhang, L.: On probabilistic automata in continuous time. In: LICS. pp. 342\u2013351. IEEE Computer Society (2010). https:\/\/doi.org\/10.1109\/LICS.2010.41","DOI":"10.1109\/LICS.2010.41"},{"key":"13_CR26","doi-asserted-by":"publisher","unstructured":"Etessami, K., Kwiatkowska, M.Z., Vardi, M.Y., Yannakakis, M.: Multi-objective model checking of Markov decision processes. LMCS 4(4) (2008). https:\/\/doi.org\/10.2168\/LMCS-4(4:8)2008","DOI":"10.2168\/LMCS-4(4:8)2008"},{"key":"13_CR27","doi-asserted-by":"publisher","unstructured":"Forejt, V., Kwiatkowska, M.Z., Norman, G., Parker, D., Qu, H.: Quantitative multi-objective verification for probabilistic systems. In: TACAS. LNCS, vol. 6605, pp. 112\u2013127. Springer (2011), https:\/\/doi.org\/10.1007\/978-3-642-19835-9_11","DOI":"10.1007\/978-3-642-19835-9_11"},{"key":"13_CR28","doi-asserted-by":"publisher","unstructured":"Forejt, V., Kwiatkowska, M.Z., Parker, D.: Pareto curves for probabilistic model checking. In: ATVA. LNCS, vol. 7561, pp. 317\u2013332. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-33386-6_25","DOI":"10.1007\/978-3-642-33386-6_25"},{"key":"13_CR29","doi-asserted-by":"publisher","unstructured":"Guck, D., Hatefi, H., Hermanns, H., Katoen, J., Timmer, M.: Analysis of timed and long-run objectives for Markov automata. LMCS 10(3) (2014). https:\/\/doi.org\/10.2168\/LMCS-10(3:17)2014","DOI":"10.2168\/LMCS-10(3:17)2014"},{"key":"13_CR30","doi-asserted-by":"publisher","unstructured":"Guck, D., Timmer, M., Hatefi, H., Ruijters, E., Stoelinga, M.: Modelling and analysis of Markov reward automata. In: ATVA. LNCS, vol. 8837, pp. 168\u2013184. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-11936-6_13","DOI":"10.1007\/978-3-319-11936-6_13"},{"key":"13_CR31","doi-asserted-by":"publisher","unstructured":"Guo, M., Zavlanos, M.M.: Probabilistic motion planning under temporal tasks and soft constraints. IEEE Trans. Autom. Control. 63(12), 4051\u20134066 (2018). https:\/\/doi.org\/10.1109\/TAC.2018.2799561","DOI":"10.1109\/TAC.2018.2799561"},{"key":"13_CR32","unstructured":"Gurobi Optimization, L.: Gurobi optimizer reference manual (2020), http:\/\/www.gurobi.com"},{"key":"13_CR33","doi-asserted-by":"publisher","unstructured":"Hahn, E.M., Hashemi, V., Hermanns, H., Lahijanian, M., Turrini, A.: Interval Markov decision processes with multiple objectives: From robust strategies to pareto curves. ACM Trans. Model. Comput. Simul. 29(4), 27:1\u201327:31 (2019). https:\/\/doi.org\/10.1145\/3309683","DOI":"10.1145\/3309683"},{"key":"13_CR34","doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Junges, S., Katoen, J., Quatmann, T.: Multi-cost bounded reachability in MDP. In: TACAS (2). LNCS, vol. 10806, pp. 320\u2013339. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_19","DOI":"10.1007\/978-3-319-89963-3_19"},{"key":"13_CR35","doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Junges, S., Katoen, J., Quatmann, T.: Multi-cost bounded tradeoff analysis in MDP. J. Autom. Reason. 64(7), 1483\u20131522 (2020). https:\/\/doi.org\/10.1007\/s10817-020-09574-9","DOI":"10.1007\/s10817-020-09574-9"},{"key":"13_CR36","doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Kaminski, B.L.: Optimistic value iteration. In: CAV (2). LNCS, vol. 12225, pp. 488\u2013511. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_26","DOI":"10.1007\/978-3-030-53291-8_26"},{"key":"13_CR37","doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Klauck, M., Parker, D., Quatmann, T., Ruijters, E.: The Quantitative Verification Benchmark Set. In: TACAS (1). LNCS, vol. 11427, pp. 344\u2013350. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-17462-0_20","DOI":"10.1007\/978-3-030-17462-0_20"},{"key":"13_CR38","doi-asserted-by":"publisher","unstructured":"Hatefi, H., Hermanns, H.: Model checking algorithms for Markov automata. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 53 (2012). https:\/\/doi.org\/10.14279\/tuj.eceasst.53.783.","DOI":"10.14279\/tuj.eceasst.53.783"},{"key":"13_CR39","doi-asserted-by":"publisher","unstructured":"Haverkort, B.R., Hermanns, H., Katoen, J.: On the use of model checking techniques for dependability evaluation. In: SRDS. pp. 228\u2013237. IEEE Computer Society (2000). https:\/\/doi.org\/10.1109\/RELDI.2000.885410","DOI":"10.1109\/RELDI.2000.885410"},{"key":"13_CR40","unstructured":"Hensel, C., Junges, S., Katoen, J., Quatmann, T., Volk, M.: The probabilistic model checker Storm. CoRR abs\/2002.07080 (2020)"},{"key":"13_CR41","doi-asserted-by":"publisher","unstructured":"Klein, J., Baier, C., Chrszon, P., Daum, M., Dubslaff, C., Kl\u00fcppelholz, S., M\u00e4rcker, S., M\u00fcller, D.: Advances in probabilistic model checking with PRISM: variable reordering, quantiles and weak deterministic b\u00fcchi automata. Int. J. Softw. Tools Technol. Transf. 20(2), 179\u2013194 (2018). https:\/\/doi.org\/10.1007\/s10009-017-0456-3","DOI":"10.1007\/s10009-017-0456-3"},{"key":"13_CR42","doi-asserted-by":"publisher","unstructured":"Kret\u00ednsk\u00fd, J., Meggendorfer, T.: Efficient strategy iteration for mean payoff in Markov decision processes. In: ATVA. LNCS, vol. 10482, pp. 380\u2013399. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-68167-2_25","DOI":"10.1007\/978-3-319-68167-2_25"},{"key":"13_CR43","doi-asserted-by":"publisher","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Santos, G.: Prism-games 3.0: Stochastic game verification with concurrency, equilibria and time. In: CAV (2). LNCS, vol. 12225, pp. 475\u2013487. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_25","DOI":"10.1007\/978-3-030-53291-8_25"},{"key":"13_CR44","doi-asserted-by":"publisher","unstructured":"Kwiatkowska, M., Parker, D., Wiltsche, C.: PRISM-games: verification and strategy synthesis for stochastic multi-player games with multiple objectives. STTT 20(2), 195\u2013210 (2018). https:\/\/doi.org\/10.1007\/s10009-017-0476-z","DOI":"10.1007\/s10009-017-0476-z"},{"key":"13_CR45","doi-asserted-by":"publisher","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: CAV. LNCS, vol. 6806, pp. 585\u2013591. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"13_CR46","doi-asserted-by":"crossref","unstructured":"Puterman, M.L.: Markov Decision Processes. John Wiley and Sons (1994)","DOI":"10.1002\/9780470316887"},{"key":"13_CR47","doi-asserted-by":"publisher","unstructured":"Quatmann, T., Junges, S., Katoen, J.: Markov automata with multiple objectives. In: CAV (1). LNCS, vol. 10426, pp. 140\u2013159. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_7","DOI":"10.1007\/978-3-319-63387-9_7"},{"key":"13_CR48","doi-asserted-by":"publisher","unstructured":"Quatmann, T., Katoen, J.: Sound value iteration. In: CAV (1). LNCS, vol. 10981, pp. 643\u2013661. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_37","DOI":"10.1007\/978-3-319-96145-3_37"},{"key":"13_CR49","doi-asserted-by":"publisher","unstructured":"Quatmann, T., Katoen, J.: Multi-objective optimization of long-run average and total rewards: Supplemental material. Zenodo (2020). https:\/\/doi.org\/10.5281\/zenodo.4094999","DOI":"10.5281\/zenodo.4094999"},{"key":"13_CR50","doi-asserted-by":"publisher","unstructured":"Randour, M., Raskin, J., Sankur, O.: Percentile queries in multi-dimensional Markov decision processes. FMSD 50(2\u20133), 207\u2013248 (2017). https:\/\/doi.org\/10.1007\/s10703-016-0262-7","DOI":"10.1007\/s10703-016-0262-7"},{"key":"13_CR51","doi-asserted-by":"publisher","unstructured":"Rennen, G., van Dam, E.R., den Hertog, D.: Enhancement of sandwich algorithms for approximating higher-dimensional convex Pareto sets. INFORMS J. Comput. 23(4), 493\u2013517 (2011). https:\/\/doi.org\/10.1287\/ijoc.1100.0419","DOI":"10.1287\/ijoc.1100.0419"},{"key":"13_CR52","unstructured":"Roijers, D.M., Scharpff, J., Spaan, M.T.J., Oliehoek, F.A., de Weerdt, M., Whiteson, S.: Bounded approximations for linear multi-objective planning under uncertainty. In: ICAPS. AAAI (2014), http:\/\/www.aaai.org\/ocs\/index.php\/ICAPS\/ICAPS14\/paper\/view\/7929"},{"key":"13_CR53","doi-asserted-by":"publisher","unstructured":"Solanki, R.S., Appino, P.A., Cohon, J.L.: Approximating the noninferior set in multiobjective linear programming problems. European Journal of Operational Research 68(3), 356\u2013373 (1993). https:\/\/doi.org\/10.1016\/0377-2217(93)90192-P","DOI":"10.1016\/0377-2217(93)90192-P"}],"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_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T00:08:47Z","timestamp":1616371727000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-72016-2_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030720155","9783030720162"],"references-count":53,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-72016-2_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"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)"}}]}}