{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,30]],"date-time":"2026-08-30T01:07:19Z","timestamp":1788052039463,"version":"build-2784847793"},"publisher-location":"Cham","reference-count":60,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031308222","type":"print"},{"value":"9783031308239","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,4,22]],"date-time":"2023-04-22T00:00:00Z","timestamp":1682121600000},"content-version":"vor","delay-in-days":111,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>Model checking undiscounted reachability and expected-reward properties on Markov decision processes (MDPs) is key for the verification of systems that act under uncertainty. Popular algorithms are policy iteration and variants of value iteration; in tool competitions, most participants rely on the latter. These algorithms generally need worst-case exponential time. However, the problem can equally be formulated as a linear program, solvable in polynomial time. In this paper, we give a detailed overview of today\u2019s state-of-the-art algorithms for MDP model checking with a focus on performance and correctness. We highlight their fundamental differences, and describe various optimizations and implementation variants. We experimentally compare floating-point and exact-arithmetic implementations of all algorithms on three benchmark sets using two probabilistic model checkers. Our results show that (optimistic) value iteration is a sensible default, but other algorithms are preferable in specific settings. This paper thereby provides a guide for MDP verification practitioners\u2014tool builders and users alike.<\/jats:p>","DOI":"10.1007\/978-3-031-30823-9_24","type":"book-chapter","created":{"date-parts":[[2023,4,21]],"date-time":"2023-04-21T16:19:12Z","timestamp":1682093952000},"page":"469-488","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":36,"title":["A Practitioner\u2019s Guide to MDP Model Checking Algorithms"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3268-8674","authenticated-orcid":false,"given":"Arnd","family":"Hartmanns","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0978-8466","authenticated-orcid":false,"given":"Sebastian","family":"Junges","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2843-5511","authenticated-orcid":false,"given":"Tim","family":"Quatmann","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0163-2152","authenticated-orcid":false,"given":"Maximilian","family":"Weininger","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2023,4,22]]},"reference":[{"key":"24_CR1","doi-asserted-by":"publisher","unstructured":"Alag\u00f6z, O., Ayvaci, M.U.S., Linderoth, J.T.: Optimally solving Markov decision processes with total expected discounted reward function: Linear programming revisited. Comput. Ind. Eng. 87, 311\u2013316 (2015). https:\/\/doi.org\/10.1016\/j.cie.2015.05.031","DOI":"10.1016\/j.cie.2015.05.031"},{"key":"24_CR2","doi-asserted-by":"publisher","unstructured":"Anand, R., Aggarwal, D., Kumar, V.: A comparative analysis of optimization solvers. Journal of Statistics and Management Systems 20(4), 623\u2013635 (2017). https:\/\/doi.org\/10.1080\/09720510.2017.1395182","DOI":"10.1080\/09720510.2017.1395182"},{"key":"24_CR3","doi-asserted-by":"publisher","unstructured":"Azeem, M., Evangelidis, A., Kret\u00ednsk\u00fd, J., Slivinskiy, A., Weininger, M.: Optimistic and topological value iteration for simple stochastic games. CoRR abs\/2207.14417 (2022). https:\/\/doi.org\/10.48550\/arXiv.2207.14417","DOI":"10.48550\/arXiv.2207.14417"},{"key":"24_CR4","doi-asserted-by":"crossref","unstructured":"Baier, C., de\u00a0Alfaro, L., Forejt, V., Kwiatkowska, M.: Model checking probabilistic systems. In: Handbook of Model Checking, pp. 963\u2013999. Springer (2018)","DOI":"10.1007\/978-3-319-10575-8_28"},{"key":"24_CR5","doi-asserted-by":"publisher","unstructured":"Baier, C., Hermanns, H., Katoen, J.P.: 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":"24_CR6","unstructured":"Baier, C., Katoen, J.P.: Principles of model checking. MIT Press (2008), https:\/\/mitpress.mit.edu\/books\/principles-model-checking"},{"key":"24_CR7","doi-asserted-by":"publisher","unstructured":"Baier, C., Klein, J., Kl\u00fcppelholz, S., M\u00e4rcker, S.: Computing conditional probabilities in Markovian models efficiently. In: TACAS. LNCS, vol.\u00a08413, pp. 515\u2013530. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_43","DOI":"10.1007\/978-3-642-54862-8_43"},{"key":"24_CR8","doi-asserted-by":"publisher","unstructured":"Baier, C., Klein, J., Leuschner, L., Parker, D., Wunderlich, S.: Ensuring the reliability of your model checker: Interval iteration for Markov decision processes. In: CAV (1). LNCS, vol. 10426, pp. 160\u2013180. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_8","DOI":"10.1007\/978-3-319-63387-9_8"},{"key":"24_CR9","doi-asserted-by":"publisher","unstructured":"Balaji, N., Kiefer, S., Novotn\u00fd, P., P\u00e9rez, G.A., Shirmohammadi, M.: On the complexity of value iteration. In: ICALP. LIPIcs, vol.\u00a0132, pp. 102:1\u2013102:15. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2019). https:\/\/doi.org\/10.4230\/LIPIcs.ICALP.2019.102","DOI":"10.4230\/LIPIcs.ICALP.2019.102"},{"key":"24_CR10","unstructured":"Berkelaar, M., Eikland, K., Notebaert, P.: Introduction to lp_solve 5.5.2.11, https:\/\/lpsolve.sourceforge.net\/5.5\/, accessed 2023-01-25."},{"key":"24_CR11","doi-asserted-by":"publisher","unstructured":"Bertsekas, D.P., Tsitsiklis, J.N.: An analysis of stochastic shortest path problems. Math. Oper. Res. 16(3), 580\u2013595 (1991). https:\/\/doi.org\/10.1287\/moor.16.3.580","DOI":"10.1287\/moor.16.3.580"},{"key":"24_CR12","unstructured":"Boyd, S.P., Vandenberghe, L.: Convex Optimization. Cambridge University Press (2014)"},{"key":"24_CR13","doi-asserted-by":"publisher","unstructured":"Br\u00e1zdil, T., Chatterjee, K., Chmelik, M., Forejt, V., Kret\u00ednsk\u00fd, J., Kwiatkowska, M.Z., Parker, D., Ujma, M.: Verification of Markov decision processes using learning algorithms. In: ATVA. LNCS, vol.\u00a08837, pp. 98\u2013114. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-11936-6_8","DOI":"10.1007\/978-3-319-11936-6_8"},{"key":"24_CR14","doi-asserted-by":"publisher","unstructured":"Budde, C.E., Hartmanns, A., Klauck, M., Kret\u00ednsk\u00fd, J., Parker, D., Quatmann, T., Turrini, A., Zhang, Z.: On correctness, precision, and performance in quantitative verification \u2013 QComp 2020 competition report. In: ISoLA (4). LNCS, vol. 12479, pp. 216\u2013241. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-83723-5_15","DOI":"10.1007\/978-3-030-83723-5_15"},{"key":"24_CR15","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Henzinger, T.A.: Value iteration. In: 25 Years of Model Checking. LNCS, vol.\u00a05000, pp. 107\u2013138. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-69850-0_7","DOI":"10.1007\/978-3-540-69850-0_7"},{"key":"24_CR16","doi-asserted-by":"publisher","unstructured":"Cubuktepe, M., Jansen, N., Junges, S., Katoen, J.P., Topcu, U.: Convex optimization for parameter synthesis in MDPs. IEEE Trans. Autom. Control. (2022). https:\/\/doi.org\/10.1109\/TAC.2021.3133265","DOI":"10.1109\/TAC.2021.3133265"},{"key":"24_CR17","unstructured":"Dai, P., Mausam, Weld, D.S., Goldsmith, J.: Topological value iteration algorithms. J. Artif. Intell. Res. 42, 181\u2013209 (2011), https:\/\/www.jair.org\/index.php\/jair\/article\/view\/10725"},{"key":"24_CR18","doi-asserted-by":"crossref","unstructured":"Dutertre, B., de\u00a0Moura, L.M.: A fast linear-arithmetic solver for DPLL(T). In: CAV. LNCS, vol.\u00a04144, pp. 81\u201394. Springer (2006)","DOI":"10.1007\/11817963_11"},{"key":"24_CR19","doi-asserted-by":"publisher","unstructured":"Eisentraut, J., Kelmendi, E., Kret\u00ednsk\u00fd, J., Weininger, M.: Value iteration for simple stochastic games: Stopping criterion and learning algorithm. Inf. Comput. 285(Part), 104886 (2022). https:\/\/doi.org\/10.1016\/j.ic.2022.104886","DOI":"10.1016\/j.ic.2022.104886"},{"key":"24_CR20","doi-asserted-by":"publisher","unstructured":"Fearnley, J.: Exponential lower bounds for policy iteration. In: ICALP (2). LNCS, vol.\u00a06199, pp. 551\u2013562. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-14162-1_46","DOI":"10.1007\/978-3-642-14162-1_46"},{"key":"24_CR21","doi-asserted-by":"publisher","unstructured":"Forejt, V., Kwiatkowska, M.Z., Parker, D.: Pareto curves for probabilistic model checking. In: ATVA. LNCS, vol.\u00a07561, 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":"24_CR22","unstructured":"Free Software Foundation: The GNU Multiple Precision Arithmetic Library, https:\/\/gmplib.org\/, accessed 2023-01-25."},{"key":"24_CR23","doi-asserted-by":"crossref","unstructured":"Funke, F., Jantsch, S., Baier, C.: Farkas certificates and minimal witnesses for probabilistic reachability constraints. In: TACAS (1). LNCS, vol. 12078, pp. 324\u2013345. Springer (2020)","DOI":"10.1007\/978-3-030-45190-5_18"},{"key":"24_CR24","unstructured":"Ge, D., Huangfu, Q., Wang, Z., Wu, J., Ye, Y.: Cardinal Optimizer (COPT) user guide (2022), https:\/\/guide.coap.online\/copt\/en-doc"},{"key":"24_CR25","unstructured":"GetFEM project: Gmm++ Library, https:\/\/getfem.org\/gmm\/, accessed 2023-01-25."},{"key":"24_CR26","doi-asserted-by":"publisher","unstructured":"Giro, S.: Optimal schedulers vs optimal bases: An approach for efficient exact solving of Markov decision processes. Theor. Comput. Sci. 538, 70\u201383 (2014). https:\/\/doi.org\/10.1016\/j.tcs.2013.08.020","DOI":"10.1016\/j.tcs.2013.08.020"},{"key":"24_CR27","doi-asserted-by":"crossref","unstructured":"Gleixner, A.M., Steffy, D.E., Wolter, K.: Improving the accuracy of linear programming solvers with iterative refinement. In: ISSAC. pp. 187\u2013194. ACM (2012)","DOI":"10.1145\/2442829.2442858"},{"key":"24_CR28","doi-asserted-by":"publisher","unstructured":"Gleixner, A.M., Steffy, D.E., Wolter, K.: Iterative refinement for linear programming. Tech. Rep.\u00a03, ZIB, Takustr. 7, 14195 Berlin (2016). https:\/\/doi.org\/10.1287\/ijoc.2016.0692","DOI":"10.1287\/ijoc.2016.0692"},{"key":"24_CR29","unstructured":"GNU Project: GLPK (GNU Linear Programming Kit), http:\/\/www.gnu.org\/software\/glpk\/glpk.html"},{"key":"24_CR30","unstructured":"Google: Glop \u2013 linear optimization, https:\/\/developers.google.com\/optimization\/lp, accessed 2023-01-25."},{"key":"24_CR31","unstructured":"Guennebaud, G., Jacob, B., et\u00a0al.: Eigen v3 (2010), http:\/\/eigen.tuxfamily.org"},{"key":"24_CR32","unstructured":"Gurobi Optimization, LLC: Gurobi Optimizer Reference Manual (2022), https:\/\/www.gurobi.com"},{"key":"24_CR33","doi-asserted-by":"crossref","unstructured":"Haddad, S., Monmege, B.: Reachability in MDPs: Refining convergence of value iteration. In: RP. LNCS, vol.\u00a08762, pp. 125\u2013137. Springer (2014)","DOI":"10.1007\/978-3-319-11439-2_10"},{"key":"24_CR34","doi-asserted-by":"publisher","unstructured":"Haddad, S., Monmege, B.: Interval iteration algorithm for MDPs and IMDPs. Theor. Comput. Sci. 735, 111\u2013131 (2018). https:\/\/doi.org\/10.1016\/j.tcs.2016.12.003","DOI":"10.1016\/j.tcs.2016.12.003"},{"key":"24_CR35","unstructured":"Hall, J., Galabova, I., Gottwald, L., Feldmeier, M.: HiGHS \u2013 high performance software for linear optimization, https:\/\/www.maths.ed.ac.uk\/hall\/HiGHS\/, accessed 2023-01-25."},{"key":"24_CR36","doi-asserted-by":"publisher","unstructured":"Hartmanns, A.: Correct probabilistic model checking with floating-point arithmetic. In: TACAS (2). LNCS, vol. 13244, pp. 41\u201359. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_3","DOI":"10.1007\/978-3-030-99527-0_3"},{"key":"24_CR37","doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Hermanns, H.: The Modest Toolset: An integrated environment for quantitative modelling and verification. In: TACAS. LNCS, vol.\u00a08413, pp. 593\u2013598. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_51","DOI":"10.1007\/978-3-642-54862-8_51"},{"key":"24_CR38","doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Junges, S., Quatmann, T., Weininger, M.: A Practitioner\u2019s Guide to MDP Model Checking Algorithms (Artefact) (2023). https:\/\/doi.org\/10.5281\/zenodo.7509474","DOI":"10.5281\/zenodo.7509474"},{"key":"24_CR39","doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Junges, S., Quatmann, T., Weininger, M.: A practitioner\u2019s guide to MDP model checking algorithms (2023). https:\/\/doi.org\/10.48550\/ARXIV.2301.10197","DOI":"10.48550\/ARXIV.2301.10197"},{"key":"24_CR40","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":"24_CR41","doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Klauck, M., Parker, D., Quatmann, T., Ruijters, E.: The quantitative verification benchmark set. In: TACAS. 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":"24_CR42","doi-asserted-by":"publisher","unstructured":"Hensel, C., Junges, S., Katoen, J.P., Quatmann, T., Volk, M.: The probabilistic model checker Storm. Int. J. Softw. Tools Technol. Transf. 24(4), 589\u2013610 (2022). https:\/\/doi.org\/10.1007\/s10009-021-00633-z","DOI":"10.1007\/s10009-021-00633-z"},{"key":"24_CR43","doi-asserted-by":"publisher","unstructured":"Huangfu, Q., Hall, J.A.J.: Parallelizing the dual revised simplex method. Math. Program. Comput. 10(1), 119\u2013142 (2018). https:\/\/doi.org\/10.1007\/s12532-017-0130-5","DOI":"10.1007\/s12532-017-0130-5"},{"key":"24_CR44","unstructured":"IBM: IBM ILOG CPLEX Optimizer, https:\/\/www.ibm.com\/analytics\/cplex-optimizer, accessed 2023-01-25."},{"key":"24_CR45","doi-asserted-by":"crossref","unstructured":"Junges, S., Torfah, H., Seshia, S.A.: Runtime monitors for Markov decision processes. In: CAV (2). LNCS, vol. 12760, pp. 553\u2013576. Springer (2021)","DOI":"10.1007\/978-3-030-81688-9_26"},{"key":"24_CR46","doi-asserted-by":"publisher","unstructured":"Kretinsky, J., Ramneantu, E., Slivinskiy, A., Weininger, M.: Comparison of algorithms for simple stochastic games. Inf. Comput. (2022). https:\/\/doi.org\/10.1016\/j.ic.2022.104885","DOI":"10.1016\/j.ic.2022.104885"},{"key":"24_CR47","doi-asserted-by":"crossref","unstructured":"Kumar, A., Zilberstein, S.: History-based controller design and optimization for partially observable MDPs. In: ICAPS. vol.\u00a025, pp. 156\u2013164 (2015)","DOI":"10.1609\/icaps.v25i1.13730"},{"key":"24_CR48","doi-asserted-by":"publisher","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D., Sproston, J.: Performance analysis of probabilistic timed automata using digital clocks. Formal Methods Syst. Des. 29(1), 33\u201378 (2006). https:\/\/doi.org\/10.1007\/s10703-006-0005-2","DOI":"10.1007\/s10703-006-0005-2"},{"key":"24_CR49","unstructured":"Littman, M.L., Dean, T.L., Kaelbling, L.P.: On the complexity of solving Markov decision problems. In: UAI. pp. 394\u2013402. Morgan Kaufmann (1995)"},{"key":"24_CR50","doi-asserted-by":"crossref","unstructured":"Mathur, U., Bauer, M.S., Chadha, R., Sistla, A.P., Viswanathan, M.: Exact quantitative probabilistic model checking through rational search. Formal Methods Syst. Des. 56(1), 90\u2013126 (2020)","DOI":"10.1007\/s10703-020-00348-y"},{"key":"24_CR51","doi-asserted-by":"publisher","unstructured":"McMahan, H.B., Likhachev, M., Gordon, G.J.: Bounded real-time dynamic programming: RTDP with monotone upper bounds and performance guarantees. In: ICML. ACM International Conference Proceeding Series, vol.\u00a0119, pp. 569\u2013576. ACM (2005). https:\/\/doi.org\/10.1145\/1102351.1102423","DOI":"10.1145\/1102351.1102423"},{"key":"24_CR52","unstructured":"MOSEK ApS: The MOSEK Optimization Suite 10.0.34, https:\/\/docs.mosek.com\/latest\/intro\/index.html, accessed 2023-01-25."},{"key":"24_CR53","doi-asserted-by":"publisher","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.S.: Z3: an efficient SMT solver. In: TACAS. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"24_CR54","doi-asserted-by":"crossref","unstructured":"Phalakarn, K., Takisaka, T., Haas, T., Hasuo, I.: Widest paths and global propagation in bounded value iteration for stochastic games. In: CAV (2). LNCS, vol. 12225, pp. 349\u2013371. Springer (2020), https:\/\/doi.org\/10.1007\/978-3-030-53291-8_19","DOI":"10.1007\/978-3-030-53291-8_19"},{"key":"24_CR55","doi-asserted-by":"publisher","unstructured":"Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley Series in Probability and Statistics, Wiley (1994). https:\/\/doi.org\/10.1002\/9780470316887","DOI":"10.1002\/9780470316887"},{"key":"24_CR56","doi-asserted-by":"publisher","unstructured":"Quatmann, T., Katoen, J.P.: 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":"24_CR57","doi-asserted-by":"crossref","unstructured":"Saad, Y., Schultz, M.H.: Gmres: a generalized minimal residual algorithm for solving nonsymmetric linear systems. Siam Journal on Scientific and Statistical Computing 7, 856\u2013869 (1986), https:\/\/epubs.siam.org\/doi\/10.1137\/0907058","DOI":"10.1137\/0907058"},{"key":"24_CR58","doi-asserted-by":"crossref","unstructured":"Wimmer, R., Jansen, N., Vorpahl, A., \u00c1brah\u00e1m, E., Katoen, J.P., Becker, B.: High-level counterexamples for probabilistic automata. Log. Methods Comput. Sci. 11(1) (2015)","DOI":"10.2168\/LMCS-11(1:15)2015"},{"key":"24_CR59","doi-asserted-by":"publisher","unstructured":"Wimmer, R., Kortus, A., Herbstritt, M., Becker, B.: Probabilistic model checking and reliability of results. In: DDECS. pp. 207\u2013212. IEEE Computer Society (2008). https:\/\/doi.org\/10.1109\/DDECS.2008.4538787","DOI":"10.1109\/DDECS.2008.4538787"},{"key":"24_CR60","doi-asserted-by":"crossref","unstructured":"Ye, Y.: The simplex and policy-iteration methods are strongly polynomial for the Markov decision problem with a fixed discount rate. Mathematics of Operations Research 36(4), 593\u2013603 (2011)","DOI":"10.1287\/moor.1110.0516"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-30823-9_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T17:05:36Z","timestamp":1781024736000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-30823-9_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031308222","9783031308239"],"references-count":60,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-30823-9_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"22 April 2023","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":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 April 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2023\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}