{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,9]],"date-time":"2026-07-09T06:40:19Z","timestamp":1783579219041,"version":"3.55.0"},"publisher-location":"Cham","reference-count":57,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783031131875","type":"print"},{"value":"9783031131882","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,8,6]],"date-time":"2022-08-06T00:00:00Z","timestamp":1659744000000},"content-version":"vor","delay-in-days":217,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We employ uncertain parametric CTMCs with parametric transition rates and a prior on the parameter values. The prior encodes uncertainty about the actual transition rates, while the parameters allow dependencies between transition rates. Sampling the parameter values from the prior distribution then yields a standard CTMC, for which we may compute relevant reachability probabilities. We provide a principled solution, based on a technique called scenario-optimization, to the following problem: From a finite set of parameter samples and a user-specified confidence level, compute prediction regions on the reachability probabilities. The prediction regions should (with high probability) contain the reachability probabilities of a CTMC induced by any additional sample. To boost the scalability of the approach, we employ standard abstraction techniques and adapt our methodology to support approximate reachability probabilities. Experiments with various well-known benchmarks show the applicability of the approach.<\/jats:p>","DOI":"10.1007\/978-3-031-13188-2_2","type":"book-chapter","created":{"date-parts":[[2022,8,5]],"date-time":"2022-08-05T08:16:57Z","timestamp":1659687417000},"page":"26-47","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":16,"title":["Sampling-Based Verification of\u00a0CTMCs with\u00a0Uncertain Rates"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5235-1967","authenticated-orcid":false,"given":"Thom S.","family":"Badings","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1318-8973","authenticated-orcid":false,"given":"Nils","family":"Jansen","sequence":"additional","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-0001-6793-8165","authenticated-orcid":false,"given":"Marielle","family":"Stoelinga","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3810-4185","authenticated-orcid":false,"given":"Matthias","family":"Volk","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2022,8,6]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"Agha, G., Palmskog, K.: A survey of statistical model checking. ACM Trans. Model. Comput. Simul. 28(1), 6:1\u20136:39 (2018)","DOI":"10.1145\/3158668"},{"issue":"2","key":"2_CR2","first-page":"128","volume":"2","author":"LJ Allen","year":"2017","unstructured":"Allen, L.J.: A primer on stochastic epidemic models: Formulation, numerical simulation, and analysis. Infect. Dis. Model. 2(2), 128\u2013142 (2017)","journal-title":"Infect. Dis. Model."},{"key":"2_CR3","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-1158-7","volume-title":"Stochastic Epidemic Models and Their Statistical Analysis","author":"H Andersson","year":"2012","unstructured":"Andersson, H., Britton, T.: Stochastic Epidemic Models and Their Statistical Analysis, vol. 151. Springer Science & Business Media, New York (2012). https:\/\/doi.org\/10.1007\/978-1-4612-1158-7"},{"issue":"1","key":"2_CR4","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1145\/343369.343402","volume":"1","author":"A Aziz","year":"2000","unstructured":"Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Model-checking continuous-time Markov chains. ACM Trans. Comput. Logic 1(1), 162\u2013170 (2000)","journal-title":"ACM Trans. Comput. Logic"},{"key":"2_CR5","doi-asserted-by":"crossref","unstructured":"Badings, T.S., Cubuktepe, M., Jansen, N., Junges, S., Katoen, J.P., Topcu, U.: Scenario-based verification of uncertain parametric MDPs. CoRR abs\/2112.13020 (2021)","DOI":"10.26226\/morressier.604907f51a80aac83ca25d97"},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"Badings, T.S., Jansen, N., Junges, S., Stoelinga, M., Volk, M.: Sampling-based verification of CTMCs with uncertain rates. Technical report, CoRR, abs\/2205.08300 (2022)","DOI":"10.1007\/978-3-031-13188-2_2"},{"issue":"6","key":"2_CR7","doi-asserted-by":"publisher","first-page":"524","DOI":"10.1109\/TSE.2003.1205180","volume":"29","author":"C Baier","year":"2003","unstructured":"Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.P.: Model-checking algorithms for continuous-time Markov chains. IEEE Trans. Softw. Eng. 29(6), 524\u2013541 (2003)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"2_CR8","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":"2_CR9","unstructured":"Bertsekas, D.P., Tsitsiklis, J.N.: Introduction to Probability. Athena Scientinis (2000)"},{"key":"2_CR10","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1016\/j.ic.2016.01.004","volume":"247","author":"L Bortolussi","year":"2016","unstructured":"Bortolussi, L., Milios, D., Sanguinetti, G.: Smoothed model checking for uncertain continuous-time Markov chains. Inf. Comput. 247, 235\u2013253 (2016)","journal-title":"Inf. Comput."},{"key":"2_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1007\/978-3-319-89963-3_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Bortolussi","year":"2018","unstructured":"Bortolussi, L., Silvetti, S.: Bayesian statistical parameter synthesis for linear temporal properties of\u00a0stochastic models. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 396\u2013413. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_23"},{"key":"2_CR12","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511804441","volume-title":"Convex Optimization","author":"S Boyd","year":"2004","unstructured":"Boyd, S., Vandenberghe, L.: Convex Optimization. Cambridge University Press, New York (2004)"},{"key":"2_CR13","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"},{"issue":"5","key":"2_CR14","doi-asserted-by":"publisher","first-page":"742","DOI":"10.1109\/TAC.2006.875041","volume":"51","author":"GC Calafiore","year":"2006","unstructured":"Calafiore, G.C., Campi, M.C.: The scenario approach to robust control design. IEEE Trans. Autom. Control. 51(5), 742\u2013753 (2006)","journal-title":"IEEE Trans. Autom. Control."},{"key":"2_CR15","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1016\/j.jss.2018.05.013","volume":"143","author":"R Calinescu","year":"2018","unstructured":"Calinescu, R., Ceska, M., Gerasimou, S., Kwiatkowska, M., Paoletti, N.: Efficient synthesis of robust models for stochastic systems. J. Syst. Softw. 143, 140\u2013158 (2018)","journal-title":"J. Syst. Softw."},{"issue":"3","key":"2_CR16","doi-asserted-by":"publisher","first-page":"1211","DOI":"10.1137\/07069821X","volume":"19","author":"MC Campi","year":"2008","unstructured":"Campi, M.C., Garatti, S.: The exact feasibility of randomized solutions of uncertain convex programs. SIAM J. Optim. 19(3), 1211\u20131230 (2008)","journal-title":"SIAM J. Optim."},{"issue":"2","key":"2_CR17","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/s10957-010-9754-6","volume":"148","author":"MC Campi","year":"2011","unstructured":"Campi, M.C., Garatti, S.: A sampling-and-discarding approach to chance-constrained optimization: feasibility and optimality. J. Optim. Theory App. 148(2), 257\u2013280 (2011)","journal-title":"J. Optim. Theory App."},{"key":"2_CR18","doi-asserted-by":"crossref","unstructured":"Campi, M.C., Garatti, S.: Introduction to the scenario approach. SIAM (2018)","DOI":"10.1137\/1.9781611975444"},{"issue":"1","key":"2_CR19","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/s10107-016-1056-9","volume":"167","author":"MC Campi","year":"2018","unstructured":"Campi, M.C., Garatti, S.: Wait-and-judge scenario optimization. Math. Program. 167(1), 155\u2013189 (2018)","journal-title":"Math. Program."},{"key":"2_CR20","doi-asserted-by":"crossref","unstructured":"Campi, M.C., Garatti, S.: Scenario optimization with relaxation: a new tool for design and application to machine learning problems. In: CDC, pp. 2463\u20132468. IEEE (2020)","DOI":"10.1109\/CDC42340.2020.9303914"},{"key":"2_CR21","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.arcontrol.2021.10.004","volume":"52","author":"M Campi","year":"2021","unstructured":"Campi, M., Car\u00e8, A., Garatti, S.: The scenario approach: a tool at the service of data-driven decision making. Ann. Rev. Control 52, 1\u201317 (2021)","journal-title":"Ann. Rev. Control"},{"key":"2_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1007\/978-3-030-85172-9_21","volume-title":"Quantitative Evaluation of Systems","author":"L Cardelli","year":"2021","unstructured":"Cardelli, L., Grosu, R., Larsen, K.G., Tribastone, M., Tschaikowski, M., Vandin, A.: Lumpability for uncertain continuous-time Markov chains. In: Abate, A., Marin, A. (eds.) QEST 2021. LNCS, vol. 12846, pp. 391\u2013409. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-85172-9_21"},{"issue":"6","key":"2_CR23","doi-asserted-by":"publisher","first-page":"589","DOI":"10.1007\/s00236-016-0265-2","volume":"54","author":"M Ceska","year":"2017","unstructured":"Ceska, M., Dannenberg, F., Paoletti, N., Kwiatkowska, M., Brim, L.: Precise parameter synthesis for stochastic biochemical systems. Acta Inform. 54(6), 589\u2013623 (2017)","journal-title":"Acta Inform."},{"key":"2_CR24","doi-asserted-by":"crossref","unstructured":"Cubuktepe, M., Jansen, N., Junges, S., Katoen, J.P., Topcu, U.: Convex optimization for parameter synthesis in MDPs. IEEE Trans Autom Control pp.\u00a01\u20131 (2022)","DOI":"10.1109\/TAC.2021.3133265"},{"key":"2_CR25","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"},{"issue":"4","key":"2_CR26","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/s10009-014-0361-y","volume":"17","author":"A David","year":"2015","unstructured":"David, A., Larsen, K.G., Legay, A., Mikucionis, M., Poulsen, D.B.: UPPAAL SMC tutorial. Int. J. Softw. Tools Technol. Transf. 17(4), 397\u2013415 (2015)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"2_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/978-3-642-22110-1_27","volume-title":"Computer Aided Verification","author":"A David","year":"2011","unstructured":"David, A., Larsen, K.G., Legay, A., Miku\u010dionis, M., Wang, Z.: Time for statistical model checking of real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 349\u2013355. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_27"},{"key":"2_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/978-3-540-31862-0_21","volume-title":"Theoretical Aspects of Computing - ICTAC 2004","author":"C Daws","year":"2005","unstructured":"Daws, C.: Symbolic and parametric model checking of discrete-time Markov chains. In: Liu, Z., Araki, K. (eds.) ICTAC 2004. LNCS, vol. 3407, pp. 280\u2013294. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31862-0_21"},{"key":"2_CR29","doi-asserted-by":"crossref","unstructured":"Domahidi, A., Chu, E., Boyd, S.P.: ECOS: an SOCP solver for embedded systems. In: ECC, pp. 3071\u20133076. IEEE (2013)","DOI":"10.23919\/ECC.2013.6669541"},{"issue":"7","key":"2_CR30","doi-asserted-by":"publisher","first-page":"607","DOI":"10.1016\/j.ifacol.2021.08.427","volume":"54","author":"S Garatti","year":"2021","unstructured":"Garatti, S., Campi, M.C.: The risk of making decisions from data through the lens of the scenario approach. IFAC-PapersOnLine 54(7), 607\u2013612 (2021)","journal-title":"IFAC-PapersOnLine"},{"key":"2_CR31","first-page":"1","volume":"191","author":"S Garatti","year":"2019","unstructured":"Garatti, S., Campi, M.: Risk and complexity in scenario optimization. Math. Program. 191, 1\u201337 (2019)","journal-title":"Math. Program."},{"issue":"1\u20132","key":"2_CR32","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1016\/S0004-3702(00)00047-3","volume":"122","author":"R Givan","year":"2000","unstructured":"Givan, R., Leach, S.M., Dean, T.L.: Bounded-parameter Markov decision processes. Artif. Intell. 122(1\u20132), 71\u2013109 (2000)","journal-title":"Artif. Intell."},{"issue":"1","key":"2_CR33","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10009-010-0146-x","volume":"13","author":"EM Hahn","year":"2011","unstructured":"Hahn, E.M., Hermanns, H., Zhang, L.: Probabilistic reachability for parametric Markov models. Int. J. Softw. Tools Technol. Transf. 13(1), 3\u201319 (2011)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"2_CR34","doi-asserted-by":"crossref","unstructured":"Han, T., Katoen, J.P., Mereacre, A.: Approximate parameter synthesis for probabilistic time-bounded reachability. In: RTSS, pp. 173\u2013182. IEEE CS (2008)","DOI":"10.1109\/RTSS.2008.19"},{"key":"2_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"344","DOI":"10.1007\/978-3-030-17462-0_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","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). https:\/\/doi.org\/10.1007\/978-3-030-17462-0_20"},{"key":"2_CR36","unstructured":"Haverkort, B.R., Hermanns, H., Katoen, J.P.: On the use of model checking techniques for dependability evaluation. In: SRDS, pp. 228\u2013237. IEEE CS (2000)"},{"key":"2_CR37","doi-asserted-by":"crossref","unstructured":"Hensel, C., Junges, S., Katoen, J.P., Quatmann, T., Volk, M.: The probabilistic model checker Storm. Softw. Tools Technol. Transf. (2021)","DOI":"10.1007\/s10009-021-00633-z"},{"key":"2_CR38","unstructured":"Hermanns, H., Meyer-Kayser, J., Siegle, M.: Multi terminal binary decision diagrams to represent and analyse continuous time Markov chains. In: 3rd International Workshop on the Numerical Solution of Markov Chains, pp. 188\u2013207. Citeseer (1999)"},{"key":"2_CR39","doi-asserted-by":"crossref","unstructured":"Jonsson, B., Larsen, K.G.: Specification and refinement of probabilistic processes. In: LICS, pp. 266\u2013277. IEEE CS (1991)","DOI":"10.1109\/LICS.1991.151651"},{"key":"2_CR40","unstructured":"Junges, S., et al.: Parameter synthesis for Markov models. CoRR abs\/1903.07993 (2019)"},{"key":"2_CR41","doi-asserted-by":"crossref","unstructured":"Katoen, J.P.: The probabilistic model checking landscape. In: LICS, pp. 31\u201345. ACM (2016)","DOI":"10.1145\/2933575.2934574"},{"key":"2_CR42","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":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., 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"},{"key":"2_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"478","DOI":"10.1007\/978-3-319-91908-9_23","volume-title":"Computing and Software Science","author":"A Legay","year":"2019","unstructured":"Legay, A., Lukina, A., Traonouez, L.M., Yang, J., Smolka, S.A., Grosu, R.: Statistical Model Checking. In: Steffen, B., Woeginger, G. (eds.) Computing and Software Science. LNCS, vol. 10000, pp. 478\u2013504. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-319-91908-9_23"},{"issue":"4","key":"2_CR44","doi-asserted-by":"publisher","first-page":"1395","DOI":"10.1007\/s10270-012-0277-5","volume":"13","author":"I Meedeniya","year":"2014","unstructured":"Meedeniya, I., Moser, I., Aleti, A., Grunske, L.: Evaluating probabilistic models with uncertain model parameters. Softw. Syst. Model. 13(4), 1395\u20131415 (2014)","journal-title":"Softw. Syst. Model."},{"key":"2_CR45","unstructured":"Mendelson, B.: Introduction to topology. Courier Corporation (1990)"},{"key":"2_CR46","doi-asserted-by":"crossref","unstructured":"Puggelli, A., Li, W., Sangiovanni-Vincentelli, A.L., Seshia, S.A.: Polynomial-time verification of PCTL properties of MDPs with convex uncertainties. In: CAV. LNCS, vol.\u00a08044, pp. 527\u2013542. Springer (2013)","DOI":"10.1007\/978-3-642-39799-8_35"},{"issue":"4","key":"2_CR47","doi-asserted-by":"publisher","first-page":"872","DOI":"10.1016\/j.ress.2008.09.007","volume":"94","author":"KD Rao","year":"2009","unstructured":"Rao, K.D., Gopika, V., Rao, V.V.S.S., Kushwaha, H.S., Verma, A.K., Srividya, A.: Dynamic fault tree analysis using Monte Carlo simulation in probabilistic safety assessment. Reliab. Eng. Syst. Saf. 94(4), 872\u2013883 (2009)","journal-title":"Reliab. Eng. Syst. Saf."},{"key":"2_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/978-3-030-94583-1_16","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R Roberts","year":"2022","unstructured":"Roberts, R., Neupane, T., Buecherl, L., Myers, C.J., Zhang, Z.: STAMINA 2.0: improving scalability of\u00a0infinite-state stochastic model checking. In: Finkbeiner, B., Wies, T. (eds.) VMCAI 2022. LNCS, vol. 13182, pp. 319\u2013331. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-94583-1_16"},{"key":"2_CR49","doi-asserted-by":"publisher","DOI":"10.1016\/j.ress.2021.107900","volume":"216","author":"R Rocchetta","year":"2021","unstructured":"Rocchetta, R., Crespo, L.G.: A scenario optimization approach to reliability-based and risk-based design: soft-constrained modulation of failure probability bounds. Reliab. Eng. Syst. Saf. 216, 107900 (2021)","journal-title":"Reliab. Eng. Syst. Saf."},{"key":"2_CR50","doi-asserted-by":"crossref","unstructured":"Ruijters, E., et al.: FFORT: a benchmark suite for fault tree analysis. In: ESREL (2019)","DOI":"10.3850\/978-981-11-2724-3_0641-cd"},{"key":"2_CR51","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/j.cosrev.2015.03.001","volume":"15","author":"E Ruijters","year":"2015","unstructured":"Ruijters, E., Stoelinga, M.I.A.: Fault tree analysis: a survey of the state-of-the-art in modeling, analysis and tools. Comput. Sci. Rev. 15, 29\u201362 (2015)","journal-title":"Comput. Sci. Rev."},{"key":"2_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/11513988_26","volume-title":"Computer Aided Verification","author":"K Sen","year":"2005","unstructured":"Sen, K., Viswanathan, M., Agha, G.: On statistical model checking of stochastic systems. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 266\u2013280. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11513988_26"},{"key":"2_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1007\/11691372_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K Sen","year":"2006","unstructured":"Sen, K., Viswanathan, M., Agha, G.: Model-checking Markov chains in the presence of uncertainties. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 394\u2013410. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11691372_26"},{"issue":"8","key":"2_CR54","doi-asserted-by":"publisher","first-page":"1314","DOI":"10.1016\/j.ijar.2009.06.007","volume":"50","author":"D Skulj","year":"2009","unstructured":"Skulj, D.: Discrete time Markov chains with interval probabilities. Int. J. Approx. Reason. 50(8), 1314\u20131329 (2009)","journal-title":"Int. J. Approx. Reason."},{"issue":"1","key":"2_CR55","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."},{"key":"2_CR56","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/978-3-030-30281-8_6","volume-title":"Quantitative Evaluation of Systems","author":"VB Wijesuriya","year":"2019","unstructured":"Wijesuriya, V.B., Abate, A.: Bayes-adaptive planning for data-efficient verification of uncertain Markov decision processes. In: Parker, D., Wolf, V. (eds.) QEST 2019. LNCS, vol. 11785, pp. 91\u2013108. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30281-8_6"},{"issue":"9","key":"2_CR57","doi-asserted-by":"publisher","first-page":"1368","DOI":"10.1016\/j.ic.2006.05.002","volume":"204","author":"HLS Younes","year":"2006","unstructured":"Younes, H.L.S., Simmons, R.G.: Statistical probabilistic model checking with a focus on time-bounded properties. Inf. Comput. 204(9), 1368\u20131409 (2006)","journal-title":"Inf. Comput."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-13188-2_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,30]],"date-time":"2024-09-30T20:21:05Z","timestamp":1727727665000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-13188-2_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031131875","9783031131882"],"references-count":57,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-13188-2_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"6 August 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Haifa","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Israel","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 August 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 August 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"34","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2022\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-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":"209","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":"40","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":"11","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":"19% - 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.9","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":"9.7","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)"}}]}}