{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,26]],"date-time":"2026-09-26T02:06:39Z","timestamp":1790388399719,"version":"4.1.0"},"publisher-location":"Cham","reference-count":78,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030175016","type":"print"},{"value":"9783030175023","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-17502-3_5","type":"book-chapter","created":{"date-parts":[[2019,4,4]],"date-time":"2019-04-04T05:19:26Z","timestamp":1554355166000},"page":"69-92","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":42,"title":["The 2019 Comparison of Tools for the Analysis of Quantitative Formal Models"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9348-7684","authenticated-orcid":false,"given":"Ernst Moritz","family":"Hahn","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3268-8674","authenticated-orcid":false,"given":"Arnd","family":"Hartmanns","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Christian","family":"Hensel","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Michaela","family":"Klauck","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4681-6964","authenticated-orcid":false,"given":"Joachim","family":"Klein","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8122-2881","authenticated-orcid":false,"given":"Jan","family":"K\u0159et\u00ednsk\u00fd","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4137-8862","authenticated-orcid":false,"given":"David","family":"Parker","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-5855-5282","authenticated-orcid":false,"given":"Enno","family":"Ruijters","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marcel","family":"Steinmetz","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2019,4,4]]},"reference":[{"key":"5_CR1","series-title":"Springer series in reliability engineering","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/978-3-319-30599-8_9","volume-title":"Principles of Performance and Reliability Modeling and Evaluation","author":"EG Amparore","year":"2016","unstructured":"Amparore, E.G., Balbo, G., Beccuti, M., Donatelli, S., Franceschinis, G.: 30 years of GreatSPN. In: Fiondella, L., Puliafito, A. (eds.) Principles of Performance and Reliability Modeling and Evaluation. SSRE, pp. 227\u2013254. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-30599-8_9"},{"key":"5_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/978-3-642-40793-2_27","volume-title":"Computer Safety, Reliability, and Security","author":"F Arnold","year":"2013","unstructured":"Arnold, F., Belinfante, A., Van der Berg, F., Guck, D., Stoelinga, M.: DFTCalc: a tool for efficient fault tree analysis. In: Bitsch, F., Guiochet, J., Ka\u00e2niche, M. (eds.) SAFECOMP 2013. LNCS, vol. 8153, pp. 293\u2013301. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40793-2_27"},{"key":"5_CR3","doi-asserted-by":"publisher","unstructured":"Babiak, T., Blahoudek, F., Duret-Lutz, A., Klein, J., Kret\u00ednsk\u00fd, J., M\u00fcller, D., Parker, D., Strejcek, J.: The Hanoi omega-automata format. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 479\u2013486. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_31","DOI":"10.1007\/978-3-319-21690-4_31"},{"key":"5_CR4","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"5_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/3-540-48320-9_12","volume-title":"CONCUR\u201999 Concurrency Theory","author":"C Baier","year":"1999","unstructured":"Baier, C., Katoen, J.-P., Hermanns, H.: Approximative symbolic model checking of continuous-time Markov chains. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 146\u2013161. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48320-9_12"},{"key":"5_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-319-63387-9_8","volume-title":"Computer Aided Verification","author":"C Baier","year":"2017","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: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 160\u2013180. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_8"},{"key":"5_CR7","unstructured":"Behrmann, G., David, A., Larsen, K.G., H\u00e5kansson, J., Pettersson, P., Yi, W., Hendriks, M.: UPPAAL 4.0. In: QEST, pp. 125\u2013126. IEEE Computer Society (2006)"},{"key":"5_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1007\/978-3-642-28756-5_38","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Beyer","year":"2012","unstructured":"Beyer, D.: Competition on software verification. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 504\u2013524. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28756-5_38"},{"issue":"10","key":"5_CR9","doi-asserted-by":"publisher","first-page":"812","DOI":"10.1109\/TSE.2006.104","volume":"32","author":"HC Bohnenkamp","year":"2006","unstructured":"Bohnenkamp, H.C., D\u2019Argenio, P.R., Hermanns, H., Katoen, J.P.: MODEST: a compositional modeling formalism for hard and softly timed systems. IEEE Trans. Softw. Eng. 32(10), 812\u2013830 (2006)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"5_CR10","unstructured":"Bonet, B., Geffner, H.: Faster heuristic search algorithms for planning with uncertainty and full feedback. In: IJCAI, pp. 1233\u20131238. Morgan Kaufmann (2003)"},{"key":"5_CR11","unstructured":"Bonet, B., Geffner, H.: Labeled RTDP: improving the convergence of real-time dynamic programming. In: ICAPS, pp. 12\u201321. AAAI (2003)"},{"key":"5_CR12","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: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 98\u2013114. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11936-6_8","DOI":"10.1007\/978-3-319-11936-6_8"},{"key":"5_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/978-3-319-69483-2_3","volume-title":"Dependable Software Engineering. Theories, Tools, and Applications","author":"CE Budde","year":"2017","unstructured":"Budde, C.E., D\u2019Argenio, P.R., Hartmanns, A.: Better automated importance splitting for transient rare events. In: Larsen, K.G., Sokolsky, O., Wang, J. (eds.) SETTA 2017. LNCS, vol. 10606, pp. 42\u201358. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-69483-2_3"},{"key":"5_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1007\/978-3-319-89963-3_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"CE Budde","year":"2018","unstructured":"Budde, C.E., D\u2019Argenio, P.R., Hartmanns, A., Sedwards, S.: A statistical model checker for nondeterminism and rare events. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 340\u2013358. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_20"},{"key":"5_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-662-54580-5_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"CE Budde","year":"2017","unstructured":"Budde, C.E., Dehnert, C., Hahn, E.M., Hartmanns, A., Junges, S., Turrini, A.: JANI: quantitative model and tool interaction. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 151\u2013168. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54580-5_9"},{"key":"5_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/978-3-319-24953-7_12","volume-title":"Automated Technology for Verification and Analysis","author":"Y Butkova","year":"2015","unstructured":"Butkova, Y., Hatefi, H., Hermanns, H., Kr\u010d\u00e1l, J.: Optimal continuous time Markov decisions. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) ATVA 2015. LNCS, vol. 9364, pp. 166\u2013182. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24953-7_12"},{"issue":"1","key":"5_CR17","first-page":"61","volume":"43","author":"T Chen","year":"2013","unstructured":"Chen, T., Forejt, V., Kwiatkowska, M.Z., Parker, D., Simaitis, A.: Automatic verification of competitive stochastic systems. FMSD 43(1), 61\u201392 (2013)","journal-title":"FMSD"},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"Coles, A.J., Coles, A., Olaya, A.G., Celorrio, S.J., Linares L\u00f3pez, C., Sanner, S., Yoon, S.: A survey of the seventh international planning competition. AI Mag. 33(1), 83\u201388 (2012)","DOI":"10.1609\/aimag.v33i1.2392"},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"Courtney, T., Gaonkar, S., Keefe, K., Rozier, E., Sanders, W.H.: M\u00f6bius 2.3: an extensible tool for dependability, security, and performance evaluation of large and complex system models. In: DSN, pp. 353\u2013358. IEEE Computer Society (2009)","DOI":"10.1109\/DSN.2009.5270318"},{"key":"5_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"336","DOI":"10.1007\/978-3-030-03421-4_22","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Verification","author":"PR D\u2019Argenio","year":"2018","unstructured":"D\u2019Argenio, P.R., Hartmanns, A., Sedwards, S.: Lightweight statistical model checking in nondeterministic continuous time. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11245, pp. 336\u2013353. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03421-4_22"},{"key":"5_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-319-11936-6_11","volume-title":"Automated Technology for Verification and Analysis","author":"C Dehnert","year":"2014","unstructured":"Dehnert, C., Jansen, N., Wimmer, R., \u00c1brah\u00e1m, E., Katoen, J.-P.: Fast debugging of PRISM models. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 146\u2013162. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11936-6_11"},{"key":"5_CR22","doi-asserted-by":"publisher","unstructured":"Dehnert, C., Junges, S., Jansen, N., Corzilius, F., Volk, M., Bruintjes, H., Katoen, J., \u00c1brah\u00e1m, E.: PROPhESY: A PRObabilistic ParamEter SYnthesis tool. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 214\u2013231. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_13","DOI":"10.1007\/978-3-319-21690-4_13"},{"key":"5_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"592","DOI":"10.1007\/978-3-319-63390-9_31","volume-title":"Computer Aided Verification","author":"C Dehnert","year":"2017","unstructured":"Dehnert, C., Junges, S., Katoen, J.-P., Volk, M.: A Storm is coming: a modern probabilistic model checker. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 592\u2013600. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_31"},{"key":"5_CR24","doi-asserted-by":"publisher","unstructured":"van Dijk, T., Hahn, E.M., Jansen, D.N., Li, Y., Neele, T., Stoelinga, M., Turrini, A., Zhang, L.: A comparative study of BDD packages for\u00a0probabilistic symbolic model checking. In: Li, X., Liu, Z., Yi, W. (eds.) SETTA 2015. LNCS, vol. 9409, pp. 35\u201351. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-25942-0_3","DOI":"10.1007\/978-3-319-25942-0_3"},{"key":"5_CR25","doi-asserted-by":"crossref","unstructured":"Eisentraut, C., Hermanns, H., Zhang, L.: On probabilistic automata in continuous time. In: LICS, pp. 342\u2013351. IEEE Computer Society (2010)","DOI":"10.1109\/LICS.2010.41"},{"key":"5_CR26","doi-asserted-by":"crossref","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":"5_CR27","unstructured":"Feng, Y., Hahn, E.M., Turrini, A., Ying, S.: Model checking omega-regular properties for quantum Markov chains. In: CONCUR. LIPIcs, vol. 85, pp. 35:1\u201335:16. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2017)"},{"key":"5_CR28","doi-asserted-by":"crossref","unstructured":"Fr\u00e4nzle, M., Hahn, E.M., Hermanns, H., Wolovick, N., Zhang, L.: Measurability and safety verification for stochastic hybrid systems. In: HSCC. ACM (2011)","DOI":"10.1145\/1967701.1967710"},{"key":"5_CR29","unstructured":"Frehse, G., Althoff, M., Bogomolov, S., Johnson, T.T. (eds.): ARCH18. 5th International Workshop on Applied Verification of Continuous and Hybrid Systems, EPiC Series in Computing, vol. 54. EasyChair (2018)"},{"key":"5_CR30","doi-asserted-by":"crossref","unstructured":"Fu, C., Turrini, A., Huang, X., Song, L., Feng, Y., Zhang, L.: Model checking probabilistic epistemic logic for probabilistic multiagent systems. In: IJCAI (2018)","DOI":"10.24963\/ijcai.2018\/661"},{"key":"5_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1007\/978-3-030-01090-4_18","volume-title":"Automated Technology for Verification and Analysis","author":"P Gainer","year":"2018","unstructured":"Gainer, P., Hahn, E.M., Schewe, S.: Accelerated model checking of parametric Markov chains. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 300\u2013316. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4_18"},{"key":"5_CR32","doi-asserted-by":"crossref","unstructured":"Gordon, A.D., Henzinger, T.A., Nori, A.V., Rajamani, S.K.: Probabilistic programming. In: FOSE, pp. 167\u2013181. ACM (2014)","DOI":"10.1145\/2593882.2593900"},{"key":"5_CR33","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1016\/j.tcs.2016.12.003","volume":"735","author":"S Haddad","year":"2018","unstructured":"Haddad, S., Monmege, B.: Interval iteration algorithm for MDPs and IMDPs. Theor. Comput. Sci. 735, 111\u2013131 (2018)","journal-title":"Theor. Comput. Sci."},{"key":"5_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/978-3-319-47677-3_6","volume-title":"Dependable Software Engineering: Theories, Tools, and Applications","author":"EM Hahn","year":"2016","unstructured":"Hahn, E.M., Hartmanns, A.: A comparison of time- and reward-bounded probabilistic model checking techniques. In: Fr\u00e4nzle, M., Kapur, D., Zhan, N. (eds.) SETTA 2016. LNCS, vol. 9984, pp. 85\u2013100. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-47677-3_6"},{"key":"5_CR35","unstructured":"Hahn, E.M., Hartmanns, A., Hermanns, H.: Reachability and reward checking for stochastic timed automata. In: Electronic Communications of the EASST, vol. 70 (2014)"},{"issue":"2","key":"5_CR36","first-page":"191","volume":"43","author":"EM Hahn","year":"2013","unstructured":"Hahn, E.M., Hartmanns, A., Hermanns, H., Katoen, J.P.: A compositional modelling and analysis framework for stochastic hybrid systems. FMSD 43(2), 191\u2013232 (2013)","journal-title":"FMSD"},{"key":"5_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-319-66335-7_13","volume-title":"Quantitative Evaluation of Systems","author":"EM Hahn","year":"2017","unstructured":"Hahn, E.M., Hashemi, V., Hermanns, H., Lahijanian, M., Turrini, A.: Multi-objective robust strategy synthesis for\u00a0interval Markov decision processes. In: Bertrand, N., Bortolussi, L. (eds.) QEST 2017. LNCS, vol. 10503, pp. 207\u2013223. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66335-7_13"},{"key":"5_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/978-3-319-43425-4_4","volume-title":"Quantitative Evaluation of Systems","author":"EM Hahn","year":"2016","unstructured":"Hahn, E.M., Hashemi, V., Hermanns, H., Turrini, A.: Exploiting robust optimization for interval probabilistic bisimulation. In: Agha, G., Van Houdt, B. (eds.) QEST 2016. LNCS, vol. 9826, pp. 55\u201371. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-43425-4_4"},{"key":"5_CR39","unstructured":"Hahn, E.M., Li, G., Schewe, S., Zhang, L.: Lazy determinisation for quantitative model checking. CoRR abs\/1311.2928 (2013)"},{"key":"5_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1007\/978-3-319-06410-9_22","volume-title":"FM 2014: Formal Methods","author":"EM Hahn","year":"2014","unstructured":"Hahn, E.M., Li, Y., Schewe, S., Turrini, A., Zhang, L.: iscasMc: a web-based probabilistic model checker. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 312\u2013317. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-06410-9_22"},{"key":"5_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/978-3-319-41540-6_16","volume-title":"Computer Aided Verification","author":"EM Hahn","year":"2016","unstructured":"Hahn, E.M., Schewe, S., Turrini, A., Zhang, L.: A simple algorithm for solving qualitative probabilistic parity games. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 291\u2013311. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_16"},{"key":"5_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"593","DOI":"10.1007\/978-3-642-54862-8_51","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Hartmanns","year":"2014","unstructured":"Hartmanns, A., Hermanns, H.: The Modest Toolset: an integrated environment for quantitative modelling and verification. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 593\u2013598. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_51"},{"key":"5_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-319-24953-7_10","volume-title":"Automated Technology for Verification and Analysis","author":"A Hartmanns","year":"2015","unstructured":"Hartmanns, A., Hermanns, H.: Explicit model checking of very large MDP using partitioning and secondary storage. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) ATVA 2015. LNCS, vol. 9364, pp. 131\u2013147. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24953-7_10"},{"key":"5_CR44","doi-asserted-by":"crossref","unstructured":"Hartmanns, A., Hermanns, H., Bungert, M.: Flexible support for time and costs in scenario-aware dataflow. In: EMSOFT, pp. 3:1\u20133:10. ACM (2016)","DOI":"10.1145\/2968478.2968496"},{"key":"5_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"320","DOI":"10.1007\/978-3-319-89963-3_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Hartmanns","year":"2018","unstructured":"Hartmanns, A., Junges, S., Katoen, J.-P., Quatmann, T.: Multi-cost bounded reachability in MDP. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 320\u2013339. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_19"},{"key":"5_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"344","DOI":"10.1007\/978-3-030-17462-0_20","volume-title":"TACAS 2019","author":"A Hartmanns","year":"2019","unstructured":"Hartmanns, A., Klauck, M., Parker, D., Quatmann, T., Ruijters, E.: The quantitative verification benchmark set. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11427, pp. 344\u2013350. Springer, Cham (2019)"},{"key":"5_CR47","unstructured":"Haslum, P., Bonet, B., Geffner, H.: New admissible heuristics for domain-independent planning. In: AAAI\/IAAI, pp. 1163\u20131168. AAAI\/MIT Press (2005)"},{"key":"5_CR48","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1613\/jair.1705","volume":"26","author":"M Helmert","year":"2006","unstructured":"Helmert, M.: The Fast Downward planning system. J. Artif. Intell. Res. 26, 191\u2013246 (2006)","journal-title":"J. Artif. Intell. Res."},{"key":"5_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/978-3-540-24622-0_8","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"T H\u00e9rault","year":"2004","unstructured":"H\u00e9rault, T., Lassaigne, R., Magniette, F., Peyronnet, S.: Approximate probabilistic model checking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 73\u201384. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24622-0_8"},{"key":"5_CR50","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511569951","volume-title":"A Compositional Approach to Performance Modelling","author":"J Hillston","year":"1996","unstructured":"Hillston, J.: A Compositional Approach to Performance Modelling. Cambridge University Press, Cambridge (1996)"},{"issue":"1","key":"5_CR51","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1609\/aimag.v33i1.2395","volume":"33","author":"M J\u00e4rvisalo","year":"2012","unstructured":"J\u00e4rvisalo, M., Berre, D.L., Roussel, O., Simon, L.: The international SAT solver competitions. AI Mag. 33(1), 89\u201392 (2012)","journal-title":"AI Mag."},{"key":"5_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"433","DOI":"10.1007\/978-3-030-03421-4_27","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Verification","author":"M Jasper","year":"2018","unstructured":"Jasper, M., Mues, M., Schl\u00fcter, M., Steffen, B., Howar, F.: RERS 2018: CTL, LTL, and reachability. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11245, pp. 433\u2013447. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03421-4_27"},{"key":"5_CR53","doi-asserted-by":"crossref","unstructured":"Klauck, M., Steinmetz, M., Hoffmann, J., Hermanns, H.: Compiling probabilistic model checking into probabilistic planning. In: ICAPS, pp. 150\u2013154. AAAI (2018)","DOI":"10.1609\/icaps.v28i1.13887"},{"key":"5_CR54","doi-asserted-by":"crossref","unstructured":"Kolobov, A., Mausam, Weld, D.S., Geffner, H.: Heuristic search for generalized stochastic shortest path MDPs. In: ICAPS. AAAI (2011)","DOI":"10.1609\/icaps.v21i1.13452"},{"issue":"2","key":"5_CR55","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/s10009-017-0476-z","volume":"20","author":"MZ Kwiatkowska","year":"2018","unstructured":"Kwiatkowska, M.Z., Parker, D., Wiltsche, C.: PRISM-games: verification and strategy synthesis for stochastic multi-player games with multiple objectives. STTT 20(2), 195\u2013210 (2018)","journal-title":"STTT"},{"key":"5_CR56","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: Game-based abstraction for Markov decision processes. In: QEST, pp. 157\u2013166. IEEE Computer Society (2006)"},{"key":"5_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"MZ Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585\u2013591. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"issue":"1","key":"5_CR58","first-page":"33","volume":"29","author":"MZ Kwiatkowska","year":"2006","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D., Sproston, J.: Performance analysis of probabilistic timed automata using digital clocks. FMSD 29(1), 33\u201378 (2006)","journal-title":"FMSD"},{"issue":"1","key":"5_CR59","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/S0304-3975(01)00046-9","volume":"282","author":"MZ Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M.Z., Norman, G., Segala, R., Sproston, J.: Automatic verification of real-time systems with discrete probability distributions. Theor. Comput. Sci. 282(1), 101\u2013150 (2002)","journal-title":"Theor. Comput. Sci."},{"key":"5_CR60","doi-asserted-by":"crossref","unstructured":"Li, Y., Liu, W., Turrini, A., Hahn, E.M., Zhang, L.: An efficient synthesis algorithm for parametric Markov chains against linear time properties. CoRR abs\/1605.04400 (2016)","DOI":"10.1007\/978-3-319-47677-3_18"},{"key":"5_CR61","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-540-30206-3_12","volume-title":"Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems","author":"O Maler","year":"2004","unstructured":"Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS\/FTRTFT -2004. LNCS, vol. 3253, pp. 152\u2013166. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30206-3_12"},{"key":"5_CR62","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"issue":"1","key":"5_CR63","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1007\/BF02883985","volume":"10","author":"M Okamoto","year":"1959","unstructured":"Okamoto, M.: Some inequalities relating to the partial sum of binomial probabilities. Ann. Inst. Stat. Math. 10(1), 29\u201335 (1959)","journal-title":"Ann. Inst. Stat. Math."},{"key":"5_CR64","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-319-46520-3_4","volume-title":"Automated Technology for Verification and Analysis","author":"T Quatmann","year":"2016","unstructured":"Quatmann, T., Dehnert, C., Jansen, N., Junges, S., Katoen, J.-P.: Parameter synthesis for Markov models: faster than ever. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 50\u201367. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46520-3_4"},{"key":"5_CR65","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-3-319-63387-9_7","volume-title":"Computer Aided Verification","author":"T Quatmann","year":"2017","unstructured":"Quatmann, T., Junges, S., Katoen, J.-P.: Markov automata with multiple objectives. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 140\u2013159. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_7"},{"key":"5_CR66","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"643","DOI":"10.1007\/978-3-319-96145-3_37","volume-title":"Computer Aided Verification","author":"T Quatmann","year":"2018","unstructured":"Quatmann, T., Katoen, J.-P.: Sound value iteration. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 643\u2013661. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_37"},{"issue":"3","key":"5_CR67","doi-asserted-by":"publisher","first-page":"22:1","DOI":"10.1145\/3161569","volume":"28","author":"D Reijsbergen","year":"2018","unstructured":"Reijsbergen, D., de Boer, P.T., Scheinhardt, W., Juneja, S.: Path-ZVA: general, efficient, and automated importance sampling for highly reliable Markovian systems. TOMACS 28(3), 22:1\u201322:25 (2018)","journal-title":"TOMACS"},{"key":"5_CR68","doi-asserted-by":"publisher","DOI":"10.1002\/9780470745403","volume-title":"Rare Event Simulation Using Monte Carlo Methods","author":"G Rubino","year":"2009","unstructured":"Rubino, G., Tuffin, B.: Rare Event Simulation Using Monte Carlo Methods. Wiley, Hoboken (2009)"},{"key":"5_CR69","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1016\/j.ress.2019.02.004","volume":"186","author":"E Ruijters","year":"2019","unstructured":"Ruijters, E., Reijsbergen, D., de Boer, P.T., Stoelinga, M.I.A.: Rare event simulation for dynamic fault trees. Reliab. Eng. Syst. Saf. 186, 220\u2013231 (2019). https:\/\/doi.org\/10.1016\/j.ress.2019.02.004","journal-title":"Reliab. Eng. Syst. Saf."},{"key":"5_CR70","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/3-540-45352-0_5","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"J Sproston","year":"2000","unstructured":"Sproston, J.: Decidable model checking of probabilistic hybrid automata. In: Joseph, M. (ed.) FTRTFT 2000. LNCS, vol. 1926, pp. 31\u201345. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-45352-0_5"},{"key":"5_CR71","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1613\/jair.5153","volume":"57","author":"M Steinmetz","year":"2016","unstructured":"Steinmetz, M., Hoffmann, J., Buffet, O.: Goal probability analysis in probabilistic planning: exploring and enhancing the state of the art. J. Artif. Intell. Res. 57, 229\u2013271 (2016)","journal-title":"J. Artif. Intell. Res."},{"key":"5_CR72","unstructured":"Sullivan, K.J., Dugan, J.B., Coppit, D.: The Galileo fault tree analysis tool. In: FTCS-29, pp. 232\u2013235. IEEE Computer Society (1999)"},{"key":"5_CR73","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/978-3-642-37075-5_23","volume-title":"Foundations of Software Science and Computation Structures","author":"M Ummels","year":"2013","unstructured":"Ummels, M., Baier, C.: Computing quantiles in Markov reward models. In: Pfenning, F. (ed.) FoSSaCS 2013. LNCS, vol. 7794, pp. 353\u2013368. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37075-5_23"},{"issue":"1","key":"5_CR74","doi-asserted-by":"publisher","first-page":"370","DOI":"10.1109\/TII.2017.2710316","volume":"14","author":"M Volk","year":"2018","unstructured":"Volk, M., Junges, S., Katoen, J.P.: Fast dynamic fault tree analysis by model checking techniques. IEEE Trans. Ind. Inform. 14(1), 370\u2013379 (2018)","journal-title":"IEEE Trans. Ind. Inform."},{"issue":"2","key":"5_CR75","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1214\/aoms\/1177731118","volume":"16","author":"A Wald","year":"1945","unstructured":"Wald, A.: Sequential tests of statistical hypotheses. Ann. Math. Stat. 16(2), 117\u2013186 (1945)","journal-title":"Ann. Math. Stat."},{"key":"5_CR76","unstructured":"Yoon, S.W., Fern, A., Givan, R.: FF-Replan: a baseline for probabilistic planning. In: ICAPS, p. 352. AAAI (2007)"},{"key":"5_CR77","doi-asserted-by":"publisher","first-page":"851","DOI":"10.1613\/jair.1880","volume":"24","author":"HLS Younes","year":"2005","unstructured":"Younes, H.L.S., Littman, M.L., Weissman, D., Asmuth, J.: The first probabilistic track of the International Planning Competition. J. Artif. Intell. Res. 24, 851\u2013887 (2005)","journal-title":"J. Artif. Intell. Res."},{"key":"5_CR78","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/3-540-45657-0_17","volume-title":"Computer Aided Verification","author":"HLS Younes","year":"2002","unstructured":"Younes, H.L.S., Simmons, R.G.: Probabilistic verification of discrete event systems using acceptance sampling. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 223\u2013235. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_17"}],"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-17502-3_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,15]],"date-time":"2023-09-15T10:50:23Z","timestamp":1694775023000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-17502-3_5"}},"subtitle":["(QComp 2019 Competition Report)"],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030175016","9783030175023"],"references-count":78,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-17502-3_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"4 April 2019","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":"Prague","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Czech Republic","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2019\/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":"164","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":"42","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":"8","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":"26% - 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":"13","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":"12 full papers and 11 short papers accepted for TOOLympics and SV-COMP (avg. 4 reviewers\/paper, selected from 43 submissions)","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)"}}]}}