{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,17]],"date-time":"2026-10-17T19:17:01Z","timestamp":1792264621831,"version":"4.4.0"},"reference-count":82,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2020,5,28]],"date-time":"2020-05-28T00:00:00Z","timestamp":1590624000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,5,28]],"date-time":"2020-05-28T00:00:00Z","timestamp":1590624000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100001834","name":"University of Twente","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100001834","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2020,12]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Statistical model checking avoids the state space explosion problem in verification and naturally supports complex non-Markovian formalisms. Yet as a simulation-based approach, its runtime becomes excessive in the presence of rare events, and it cannot soundly analyse nondeterministic models. In this article, we present : a statistical model checker that combines fully automated importance splitting to estimate the probabilities of rare events with smart lightweight scheduler sampling to approximate optimal schedulers in nondeterministic models. As part of the <jats:sc>Modest Toolset<\/jats:sc>, it supports a variety of input formalisms natively and via the <jats:sc>Jani<\/jats:sc> exchange format. A modular software architecture allows its various features to be flexibly combined. We highlight its capabilities using experiments across multi-core and distributed setups on three case studies and report on an extensive performance comparison with three current statistical model checkers.\n<\/jats:p>","DOI":"10.1007\/s10009-020-00563-2","type":"journal-article","created":{"date-parts":[[2020,5,28]],"date-time":"2020-05-28T10:02:57Z","timestamp":1590660177000},"page":"759-780","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":42,"title":["An efficient statistical model checker for nondeterminism and rare events"],"prefix":"10.1007","volume":"22","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8807-1548","authenticated-orcid":false,"given":"Carlos E.","family":"Budde","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8528-9215","authenticated-orcid":false,"given":"Pedro R.","family":"D\u2019Argenio","sequence":"additional","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"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2903-0823","authenticated-orcid":false,"given":"Sean","family":"Sedwards","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2020,5,28]]},"reference":[{"issue":"1","key":"563_CR1","doi-asserted-by":"publisher","first-page":"6:1","DOI":"10.1145\/3158668","volume":"28","author":"G Agha","year":"2018","unstructured":"Agha, G., Palmskog, K.: A survey of statistical model checking. ACM Trans. Model. Comput. Simul. 28(1), 6:1\u20136:39 (2018). https:\/\/doi.org\/10.1145\/3158668","journal-title":"ACM Trans. Model. Comput. Simul."},{"issue":"2","key":"563_CR2","doi-asserted-by":"publisher","first-page":"119","DOI":"10.2307\/2685469","volume":"52","author":"A Agresti","year":"1998","unstructured":"Agresti, A., Coull, B.A.: Approximate is better than \u201cexact\u201d for interval estimation of binomial proportions. Am. Stat. 52(2), 119\u2013126 (1998). https:\/\/doi.org\/10.2307\/2685469","journal-title":"Am. Stat."},{"issue":"2","key":"563_CR3","doi-asserted-by":"publisher","first-page":"13:1","DOI":"10.1145\/1899396.1899401","volume":"21","author":"M Amrein","year":"2011","unstructured":"Amrein, M., K\u00fcnsch, H.R.: A variant of importance splitting for rare event estimation: fixed number of successes. ACM Trans. Model. Comput. Simul. 21(2), 13:1\u201313:20 (2011). https:\/\/doi.org\/10.1145\/1899396.1899401","journal-title":"ACM Trans. Model. Comput. Simul."},{"key":"563_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":"563_CR5","doi-asserted-by":"publisher","unstructured":"Bogdoll, J., Hartmanns, A., Hermanns, H.: Simulation and statistical model checking for Modestly nondeterministic models. In: MMB\/DFT, LNCS, vol. 7201, pp. 249\u2013252. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-28540-0_20","DOI":"10.1007\/978-3-642-28540-0_20"},{"issue":"10","key":"563_CR6","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.: MoDeST: a compositional modeling formalism for hard and softly timed systems. IEEE Trans. Softw. Eng. 32(10), 812\u2013830 (2006). https:\/\/doi.org\/10.1109\/TSE.2006.104","journal-title":"IEEE Trans. Softw. Eng."},{"key":"563_CR7","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. 8837, 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":"563_CR8","unstructured":"Budde, C.E.: Automation of importance splitting techniques for rare event simulation. Ph.D. thesis, Universidad Nacional de C\u00f3rdoba, C\u00f3rdoba, Argentina (2017)"},{"key":"563_CR9","doi-asserted-by":"publisher","unstructured":"Budde, C.E., D\u2019Argenio, P.R., Hartmanns, A.: Better automated importance splitting for transient rare events. In: SETTA, LNCS, vol. 10606, pp. 42\u201358. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-69483-2_3","DOI":"10.1007\/978-3-319-69483-2_3"},{"key":"563_CR10","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1016\/j.scico.2019.01.006","volume":"174","author":"CE Budde","year":"2019","unstructured":"Budde, C.E., D\u2019Argenio, P.R., Hartmanns, A.: Automated compositional importance splitting. Sci. Comput. Program. 174, 90\u2013108 (2019). https:\/\/doi.org\/10.1016\/j.scico.2019.01.006","journal-title":"Sci. Comput. Program."},{"key":"563_CR11","doi-asserted-by":"publisher","unstructured":"Budde, C.E., D\u2019Argenio, P.R., Hartmanns, A., Sedwards, S.: A statistical model checker for nondeterminism and rare events. In: TACAS, LNCS, vol. 10806, pp. 340\u2013358. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_20","DOI":"10.1007\/978-3-319-89963-3_20"},{"key":"563_CR12","doi-asserted-by":"publisher","unstructured":"Budde, C.E., D\u2019Argenio, P.R., Monti, R.E.: Compositional construction of importance functions in fully automated importance splitting. In: VALUETOOLS. ICST (2016). https:\/\/doi.org\/10.4108\/eai.25-10-2016.2266501","DOI":"10.4108\/eai.25-10-2016.2266501"},{"key":"563_CR13","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, LNCS, vol. 10206, pp. 151\u2013168. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-662-54580-5_9","DOI":"10.1007\/978-3-662-54580-5_9"},{"key":"563_CR14","doi-asserted-by":"publisher","unstructured":"Bulychev, P.E., David, A., Larsen, K.G., Legay, A., Mikucionis, M., Poulsen, D.B.: Checking and distributing statistical model checking. In: NASA Formal Methods, LNCS, vol. 7226, pp. 449\u2013463. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-28891-3_39","DOI":"10.1007\/978-3-642-28891-3_39"},{"issue":"3","key":"563_CR15","doi-asserted-by":"publisher","first-page":"795","DOI":"10.1007\/s11222-011-9231-6","volume":"22","author":"F C\u00e9rou","year":"2012","unstructured":"C\u00e9rou, F., Del Moral, P., Furon, T., Guyader, A.: Sequential Monte Carlo for rare event estimation. Stat. Comput. 22(3), 795\u2013808 (2012). https:\/\/doi.org\/10.1007\/s11222-011-9231-6","journal-title":"Stat. Comput."},{"key":"563_CR16","doi-asserted-by":"publisher","unstructured":"Chen, J., Xu, J.: Sampling adaptively using the Massart inequality for scalable learning. In: ICMLA, pp. 362\u2013367. IEEE (2013). https:\/\/doi.org\/10.1109\/ICMLA.2013.149","DOI":"10.1109\/ICMLA.2013.149"},{"issue":"2","key":"563_CR17","doi-asserted-by":"publisher","first-page":"457","DOI":"10.1214\/aoms\/1177700156","volume":"36","author":"YS Chow","year":"1965","unstructured":"Chow, Y.S., Robbins, H.: On the asymptotic theory of fixed-width sequential confidence intervals for the mean. Ann. Math. Stat. 36(2), 457\u2013462 (1965). https:\/\/doi.org\/10.1214\/aoms\/1177700156","journal-title":"Ann. Math. Stat."},{"issue":"4","key":"563_CR18","doi-asserted-by":"publisher","first-page":"404","DOI":"10.2307\/2331986","volume":"26","author":"CJ Clopper","year":"1934","unstructured":"Clopper, C.J., Pearson, E.S.: The use of confidence or fiducial limits illustrated in the case of the binomial. Biometrika 26(4), 404\u2013413 (1934). https:\/\/doi.org\/10.2307\/2331986","journal-title":"Biometrika"},{"issue":"2","key":"563_CR19","doi-asserted-by":"publisher","first-page":"12:1","DOI":"10.1145\/3060139","volume":"18","author":"P Daca","year":"2017","unstructured":"Daca, P., Henzinger, T.A., Kret\u00ednsk\u00fd, J., Petrov, T.: Faster statistical model checking for unbounded temporal properties. ACM Trans. Comput. Log. 18(2), 12:1\u201312:25 (2017). https:\/\/doi.org\/10.1145\/3060139","journal-title":"ACM Trans. Comput. Log."},{"key":"563_CR20","doi-asserted-by":"publisher","unstructured":"D\u2019Argenio, P.R., Gerhold, M., Hartmanns, A., Sedwards, S.: A hierarchy of scheduler classes for stochastic automata. In: FoSSaCS, LNCS, vol. 10803. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-89366-2_21","DOI":"10.1007\/978-3-319-89366-2_21"},{"key":"563_CR21","doi-asserted-by":"publisher","unstructured":"D\u2019Argenio, P.R., Hartmanns, A., Legay, A., Sedwards, S.: Statistical approximation of optimal schedulers for probabilistic timed automata. In: iFM, LNCS, vol. 9681, pp. 99\u2013114. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-33693-0_7","DOI":"10.1007\/978-3-319-33693-0_7"},{"key":"563_CR22","doi-asserted-by":"publisher","unstructured":"D\u2019Argenio, P.R., Hartmanns, A., Sedwards, S.: Lightweight statistical model checking in nondeterministic continuous time. In: ISoLA, LNCS, vol. 11245, pp. 336\u2013353. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-030-03421-4_22","DOI":"10.1007\/978-3-030-03421-4_22"},{"issue":"1","key":"563_CR23","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.ic.2005.07.001","volume":"203","author":"PR D\u2019Argenio","year":"2005","unstructured":"D\u2019Argenio, P.R., Katoen, J.P.: A theory of stochastic systems part I: stochastic automata. Inf. Comput. 203(1), 1\u201338 (2005). https:\/\/doi.org\/10.1016\/j.ic.2005.07.001","journal-title":"Inf. Comput."},{"issue":"4","key":"563_CR24","doi-asserted-by":"publisher","first-page":"469","DOI":"10.1007\/s10009-015-0383-0","volume":"17","author":"PR D\u2019Argenio","year":"2015","unstructured":"D\u2019Argenio, P.R., Legay, A., Sedwards, S., Traonouez, L.M.: Smart sampling for lightweight verification of Markov decision processes. STTT 17(4), 469\u2013484 (2015). https:\/\/doi.org\/10.1007\/s10009-015-0383-0","journal-title":"STTT"},{"key":"563_CR25","doi-asserted-by":"publisher","unstructured":"David, A., Jensen, P.G., Larsen, K.G., Mikucionis, M., Taankvist, J.H.: Uppaal stratego. In: TACAS, LNCS, vol. 9035, pp. 206\u2013211. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_16","DOI":"10.1007\/978-3-662-46681-0_16"},{"key":"563_CR26","doi-asserted-by":"publisher","unstructured":"David, A., Larsen, K.G., Legay, A., Mikucionis, M., Wang, Z.: Time for statistical model checking of real-time systems. In: CAV, LNCS, vol. 6806, pp. 349\u2013355. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_27","DOI":"10.1007\/978-3-642-22110-1_27"},{"issue":"2","key":"563_CR27","doi-asserted-by":"publisher","first-page":"562","DOI":"10.1016\/j.spa.2008.02.017","volume":"119","author":"T Dean","year":"2009","unstructured":"Dean, T., Dupuis, P.: Splitting for rare event simulation: a large deviation approach to design and analysis. Stoch. Process. Appl. 119(2), 562\u2013587 (2009). https:\/\/doi.org\/10.1016\/j.spa.2008.02.017","journal-title":"Stoch. Process. Appl."},{"key":"563_CR28","doi-asserted-by":"publisher","unstructured":"Dehnert, C., Junges, S., Katoen, J.P., Volk, M.: A Storm is coming: A modern probabilistic model checker. In: CAV, LNCS, vol. 10427, pp. 592\u2013600. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_31","DOI":"10.1007\/978-3-319-63390-9_31"},{"key":"563_CR29","doi-asserted-by":"publisher","unstructured":"Dombrowski, C., Junges, S., Katoen, J.P., Gross, J.: Model-checking assisted protocol design for ultra-reliable low-latency wireless networks. In: SRDS, pp. 307\u2013316. IEEE (2016). https:\/\/doi.org\/10.1109\/SRDS.2016.048","DOI":"10.1109\/SRDS.2016.048"},{"key":"563_CR30","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":"563_CR31","doi-asserted-by":"publisher","unstructured":"Forejt, V., Kwiatkowska, M.Z., Norman, G., Parker, D.: Automated verification techniques for probabilistic systems. In: SFM, LNCS, vol. 6659, pp. 53\u2013113. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-21455-4_3","DOI":"10.1007\/978-3-642-21455-4_3"},{"key":"563_CR32","doi-asserted-by":"publisher","unstructured":"Fr\u00e4nzle, M., Hahn, E.M., Hermanns, H., Wolovick, N., Zhang, L.: Measurability and safety verification for stochastic hybrid systems. In: HSCC, pp. 43\u201352. ACM (2011). https:\/\/doi.org\/10.1145\/1967701.1967710","DOI":"10.1145\/1967701.1967710"},{"issue":"3","key":"563_CR33","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1198\/tast.2010.09140","volume":"64","author":"J Frey","year":"2010","unstructured":"Frey, J.: Fixed-width sequential confidence intervals for a proportion. Am. Stat. 64(3), 242\u2013249 (2010). https:\/\/doi.org\/10.1198\/tast.2010.09140","journal-title":"Am. Stat."},{"key":"563_CR34","unstructured":"Garvels, M.J.J.: The splitting method in rare event simulation. Ph.D. thesis, University of Twente, Enschede, The Netherlands (2000)"},{"key":"563_CR35","doi-asserted-by":"publisher","unstructured":"Garvels, M.J.J., Kroese, D.P.: A comparison of RESTART implementations. In: Winter Simulation Conference, pp. 601\u2013608 (1998). https:\/\/doi.org\/10.1109\/WSC.1998.745040","DOI":"10.1109\/WSC.1998.745040"},{"issue":"4","key":"563_CR36","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1002\/ett.4460130408","volume":"13","author":"MJJ Garvels","year":"2002","unstructured":"Garvels, M.J.J., van Ommeren, J.C.W., Kroese, D.P.: On the importance function in splitting simulation. Eur. Trans. Telecommun. 13(4), 363\u2013371 (2002). https:\/\/doi.org\/10.1002\/ett.4460130408","journal-title":"Eur. Trans. Telecommun."},{"issue":"1","key":"563_CR37","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1109\/12.123381","volume":"41","author":"A Goyal","year":"1992","unstructured":"Goyal, A., Shahabuddin, P., Heidelberger, P., Nicola, V.F., Glynn, P.W.: A unified framework for simulating Markovian models of highly dependable systems. IEEE Trans. Comput. 41(1), 36\u201351 (1992). https:\/\/doi.org\/10.1109\/12.123381","journal-title":"IEEE Trans. Comput."},{"key":"563_CR38","doi-asserted-by":"publisher","unstructured":"Graf-Brill, A., Hartmanns, A., Hermanns, H., Rose, S.: Modelling and certification for electric mobility. In: Industrial Informatics (INDIN). IEEE (2017). https:\/\/doi.org\/10.1109\/INDIN.2017.8104755","DOI":"10.1109\/INDIN.2017.8104755"},{"issue":"2","key":"563_CR39","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/s10703-012-0167-z","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. Formal Methods Syst. Des. 43(2), 191\u2013232 (2013). https:\/\/doi.org\/10.1007\/s10703-012-0167-z","journal-title":"Formal Methods Syst. Des."},{"key":"563_CR40","doi-asserted-by":"publisher","unstructured":"Hartmanns, A.: A statistical model checker for nondeterminism and rare events (artifact). 4TU. Centre for Research Data (2018). https:\/\/doi.org\/10.4121\/uuid:64cd25f4-4192-46d1-a951-9f99b452b48f","DOI":"10.4121\/uuid:64cd25f4-4192-46d1-a951-9f99b452b48f"},{"key":"563_CR41","doi-asserted-by":"publisher","unstructured":"Hartmanns, A.: An efficient statistical model checker for nondeterminism and rare events (artifact). 4TU.Centre for Research Data (2019). https:\/\/doi.org\/10.4121\/uuid:2896b362-85d8-4705-bbe4-073fc79e23ec","DOI":"10.4121\/uuid:2896b362-85d8-4705-bbe4-073fc79e23ec"},{"key":"563_CR42","doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Hensel, C., Klauck, M., Klein, J., Kret\u00ednsk\u00fd, J., Parker, D., Quatmann, T., Ruijters, E., Steinmetz, M.: The 2019 comparison of tools for the analysis of quantitative formal models. In: TACAS, LNCS, vol. 11429. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-17502-3_5","DOI":"10.1007\/978-3-030-17502-3_5"},{"key":"563_CR43","doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Hermanns, H.: The Modest Toolset: An integrated environment for quantitative modelling and verification. In: TACAS, LNCS, vol. 8413, 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":"563_CR44","doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Hermanns, H., Bungert, M.: Flexible support for time and costs in scenario-aware dataflow. In: EMSOFT. ACM (2016). https:\/\/doi.org\/10.1145\/2968478.2968496","DOI":"10.1145\/2968478.2968496"},{"key":"563_CR45","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. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-17462-0_20","DOI":"10.1007\/978-3-030-17462-0_20"},{"key":"563_CR46","doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Sedwards, S., D\u2019Argenio, P.R.: Efficient simulation-based verification of probabilistic timed automata. In: Winter Simulation Conference (2017). https:\/\/doi.org\/10.1109\/WSC.2017.8247885","DOI":"10.1109\/WSC.2017.8247885"},{"issue":"4","key":"563_CR47","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1007\/s10009-014-0349-7","volume":"17","author":"A Hartmanns","year":"2015","unstructured":"Hartmanns, A., Timmer, M.: Sound statistical model checking for MDP using partial order and confluence reduction. STTT 17(4), 429\u2013456 (2015). https:\/\/doi.org\/10.1007\/s10009-014-0349-7","journal-title":"STTT"},{"issue":"1","key":"563_CR48","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1006\/jcss.1998.1581","volume":"57","author":"TA Henzinger","year":"1998","unstructured":"Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What\u2019s decidable about hybrid automata? J. Comput. Syst. Sci. 57(1), 94\u2013124 (1998). https:\/\/doi.org\/10.1006\/jcss.1998.1581","journal-title":"J. Comput. Syst. Sci."},{"key":"563_CR49","doi-asserted-by":"publisher","unstructured":"H\u00e9rault, T., Lassaigne, R., Magniette, F., Peyronnet, S.: Approximate probabilistic model checking. In: VMCAI, LNCS, vol. 2937, pp. 73\u201384. Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-24622-0_8","DOI":"10.1007\/978-3-540-24622-0_8"},{"key":"563_CR50","doi-asserted-by":"publisher","unstructured":"H\u00fcls, J., Remke, A.: Coordinated charging strategies for plug-in electric vehicles to ensure a robust charging process. In: VALUETOOLS. ICST (2016). https:\/\/doi.org\/10.4108\/eai.25-10-2016.2266997","DOI":"10.4108\/eai.25-10-2016.2266997"},{"key":"563_CR51","doi-asserted-by":"publisher","unstructured":"J\u00e9gourel, C., Larsen, K.G., Legay, A., Mikucionis, M., Poulsen, D.B., Sedwards, S.: Importance sampling for stochastic timed automata. In: SETTA, LNCS, vol. 9984, pp. 163\u2013178. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-47677-3_11","DOI":"10.1007\/978-3-319-47677-3_11"},{"key":"563_CR52","doi-asserted-by":"publisher","unstructured":"J\u00e9gourel, C., Legay, A., Sedwards, S.: Importance splitting for statistical model checking rare properties. In: CAV, LNCS, vol. 8044, pp. 576\u2013591. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_38","DOI":"10.1007\/978-3-642-39799-8_38"},{"key":"563_CR53","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.tcs.2016.08.009","volume":"649","author":"C J\u00e9gourel","year":"2016","unstructured":"J\u00e9gourel, C., Legay, A., Sedwards, S.: Command-based importance sampling for statistical model checking. Theor. Comput. Sci. 649, 1\u201324 (2016). https:\/\/doi.org\/10.1016\/j.tcs.2016.08.009","journal-title":"Theor. Comput. Sci."},{"key":"563_CR54","doi-asserted-by":"publisher","unstructured":"J\u00e9gourel, C., Legay, A., Sedwards, S., Traonouez, L.M.: Distributed verification of rare properties using importance splitting observers. ECEASST 72 (2015). https:\/\/doi.org\/10.14279\/tuj.eceasst.72.1024","DOI":"10.14279\/tuj.eceasst.72.1024"},{"issue":"2\u20133","key":"563_CR55","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1023\/A:1017932429737","volume":"49","author":"MJ Kearns","year":"2002","unstructured":"Kearns, M.J., Mansour, Y., Ng, A.Y.: A sparse sampling algorithm for near-optimal planning in large Markov decision processes. Mach. Learn. 49(2\u20133), 193\u2013208 (2002). https:\/\/doi.org\/10.1023\/A:1017932429737","journal-title":"Mach. Learn."},{"issue":"4","key":"563_CR56","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1145\/1096166.1096174","volume":"9","author":"S Kurkowski","year":"2005","unstructured":"Kurkowski, S., Camp, T., Colagrosso, M.: MANET simulation studies: the incredibles. Mobile Comput. Commun. Rev. 9(4), 50\u201361 (2005). https:\/\/doi.org\/10.1145\/1096166.1096174","journal-title":"Mobile Comput. Commun. Rev."},{"key":"563_CR57","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"},{"issue":"1","key":"563_CR58","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). https:\/\/doi.org\/10.1016\/S0304-3975(01)00046-9","journal-title":"Theor. Comput. Sci."},{"key":"563_CR59","doi-asserted-by":"publisher","unstructured":"L\u2019Ecuyer, P., Le Gland, F., Lezaud, P., Tuffin, B.: Splitting techniques. In: Rubino, G., Tuffin, B. (eds.) Rare Event Simulation Using Monte Carlo Methods, pp. 39\u201361. Wiley (2009). https:\/\/doi.org\/10.1002\/9780470745403.ch3","DOI":"10.1002\/9780470745403.ch3"},{"key":"563_CR60","doi-asserted-by":"publisher","unstructured":"Legay, A., Sedwards, S., Traonouez, L.: Scalable verification of Markov decision processes. In: WS-FMDS at SEFM, LNCS, vol. 8938, pp. 350\u2013362. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-15201-1_23","DOI":"10.1007\/978-3-319-15201-1_23"},{"key":"563_CR61","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-3-319-47166-2_6","volume":"9952","author":"A Legay","year":"2016","unstructured":"Legay, A., Sedwards, S., Traonouez, L.M.: Plasma Lab: a modular statistical model checking platform. ISoLA, LNCS 9952, 77\u201393 (2016). https:\/\/doi.org\/10.1007\/978-3-319-47166-2_6","journal-title":"ISoLA, LNCS"},{"key":"563_CR62","doi-asserted-by":"publisher","unstructured":"Legay, A., Sedwards, S., Traonouez, L.M.: Rare events for statistical model checking an overview. In: Reachability Problems, LNCS, vol. 9899, pp. 23\u201335. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-45994-3_2","DOI":"10.1007\/978-3-319-45994-3_2"},{"key":"563_CR63","doi-asserted-by":"publisher","unstructured":"LeGland, F., Oudjane, N.: A sequential particle algorithm that keeps the particle system alive, pp. 351\u2013389. Springer (2006). https:\/\/doi.org\/10.1007\/11587392_11","DOI":"10.1007\/11587392_11"},{"issue":"1","key":"563_CR64","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1145\/272991.272995","volume":"8","author":"M Matsumoto","year":"1998","unstructured":"Matsumoto, M., Nishimura, T.: Mersenne twister: A 623-dimensionally equidistributed uniform pseudo-random number generator. ACM Trans. Model. Comput. Simul. 8(1), 3\u201330 (1998). https:\/\/doi.org\/10.1145\/272991.272995","journal-title":"ACM Trans. Model. Comput. Simul."},{"key":"563_CR65","unstructured":"Nimal, V.: Statistical approaches for probabilistic model checking. Master\u2019s thesis, Oxford University (2010)"},{"issue":"1","key":"563_CR66","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). https:\/\/doi.org\/10.1007\/BF02883985","journal-title":"Ann. Inst. Stat. Math."},{"key":"563_CR67","doi-asserted-by":"publisher","unstructured":"Pilch, C., Remke, A.: Statistical model checking for hybrid Petri nets with multiple general transitions. In: DSN, pp. 475\u2013486. IEEE Computer Society (2017). https:\/\/doi.org\/10.1109\/DSN.2017.41","DOI":"10.1109\/DSN.2017.41"},{"key":"563_CR68","doi-asserted-by":"crossref","unstructured":"Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley Series in Probability and Mathematical Statistics: Applied Probability and Statistics. Wiley, New York (1994)","DOI":"10.1002\/9780470316887"},{"key":"563_CR69","doi-asserted-by":"publisher","unstructured":"Reijsbergen, D., de\u00a0Boer, P., Scheinhardt, W.R.W.: Hypothesis testing for rare-event simulation: Limitations and possibilities. In: ISoLA, LNCS, vol. 9952, pp. 16\u201326. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-47166-2_2","DOI":"10.1007\/978-3-319-47166-2_2"},{"issue":"4","key":"563_CR70","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/s10009-014-0350-1","volume":"17","author":"D Reijsbergen","year":"2015","unstructured":"Reijsbergen, D., de Boer, P., Scheinhardt, W.R.W., Haverkort, B.R.: On hypothesis testing for statistical model checking. STTT 17(4), 377\u2013395 (2015). https:\/\/doi.org\/10.1007\/s10009-014-0350-1","journal-title":"STTT"},{"key":"563_CR71","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1016\/j.jcp.2014.12.009","volume":"283","author":"J Rolland","year":"2015","unstructured":"Rolland, J., Simonnet, E.: Statistical behaviour of adaptive multilevel splitting algorithms in simple models. J. Comput. Phys. 283, 541\u2013558 (2015). https:\/\/doi.org\/10.1016\/j.jcp.2014.12.009","journal-title":"J. Comput. Phys."},{"key":"563_CR72","doi-asserted-by":"publisher","unstructured":"Rubino, G., Tuffin, B.: Introduction to Rare Event Simulation. In: In: Rubino, G., Tuffin, B. (eds.) Rare Event Simulation Using Monte Carlo Methods, pp. 1\u201313. Wiley (2009). https:\/\/doi.org\/10.1002\/9780470745403.ch1","DOI":"10.1002\/9780470745403.ch1"},{"issue":"1","key":"563_CR73","doi-asserted-by":"publisher","first-page":"817","DOI":"10.1214\/14-EJS909","volume":"8","author":"M Thulin","year":"2014","unstructured":"Thulin, M.: The cost of using exact confidence intervals for a binomial proportion. Electron. J. Stat. 8(1), 817\u2013840 (2014). https:\/\/doi.org\/10.1214\/14-EJS909","journal-title":"Electron. J. Stat."},{"issue":"C","key":"563_CR74","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/j.ress.2016.04.020","volume":"154","author":"P Turati","year":"2016","unstructured":"Turati, P., Pedroni, N., Zio, E.: Advanced RESTART method for the estimation of the probability of failure of highly reliable hybrid dynamic systems. Reliab. Eng. Syst. Safety 154(C), 117\u2013126 (2016). https:\/\/doi.org\/10.1016\/j.ress.2016.04.020","journal-title":"Reliab. Eng. Syst. Safety"},{"key":"563_CR75","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1016\/j.peva.2018.02.002","volume":"121\u2013122","author":"J Vill\u00e9n-Altamirano","year":"2018","unstructured":"Vill\u00e9n-Altamirano, J.: RESTART vs splitting: a comparative study. Perform. Eval. 121\u2013122, 38\u201347 (2018). https:\/\/doi.org\/10.1016\/j.peva.2018.02.002","journal-title":"Perform. Eval."},{"key":"563_CR76","unstructured":"Vill\u00e9n-Altamirano, M., Vill\u00e9n-Altamirano, J.: RESTART: a method for accelerating rare event simulations. In: Queueing, Performance and Control in ATM (ITC-13), pp. 71\u201376. Elsevier (1991)"},{"key":"563_CR77","doi-asserted-by":"publisher","unstructured":"Vill\u00e9n-Altamirano, M., Vill\u00e9n-Altamirano, J.: The rare event simulation method RESTART: efficiency analysis and guidelines for its application. In: Network Performance Engineering, LNCS, vol. 5233, pp. 509\u2013547. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-02742-0_22","DOI":"10.1007\/978-3-642-02742-0_22"},{"issue":"2","key":"563_CR78","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). https:\/\/doi.org\/10.1214\/aoms\/1177731118","journal-title":"Ann. Math. Stat."},{"issue":"3","key":"563_CR79","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1214\/aoms\/1177730197","volume":"19","author":"A Wald","year":"1948","unstructured":"Wald, A., Wolfowitz, J.: Optimum character of the sequential probability ratio test. Ann. Math. Stat. 19(3), 326\u2013339 (1948). https:\/\/doi.org\/10.1214\/aoms\/1177730197","journal-title":"Ann. Math. Stat."},{"key":"563_CR80","doi-asserted-by":"publisher","unstructured":"Younes, H.L.S.: Ymer: A statistical model checker. In: CAV, LNCS, vol. 3576, pp. 429\u2013433. Springer (2005). https:\/\/doi.org\/10.1007\/11513988_43","DOI":"10.1007\/11513988_43"},{"key":"563_CR81","doi-asserted-by":"publisher","unstructured":"Younes, H.L.S., Simmons, R.G.: Probabilistic verification of discrete event systems using acceptance sampling. In: CAV, vol. 2404, pp. 223\u2013235. Springer (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_17","DOI":"10.1007\/3-540-45657-0_17"},{"key":"563_CR82","doi-asserted-by":"publisher","unstructured":"Zimmermann, A., Lavista, A.C., Rodr\u00edguez, R.J.: Some notes on rare-event simulation challenges. In: VALUETOOLS, pp. 263\u2013264. ACM (2017). https:\/\/doi.org\/10.1145\/3150928.3150963","DOI":"10.1145\/3150928.3150963"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-020-00563-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-020-00563-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-020-00563-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,28]],"date-time":"2021-05-28T00:44:43Z","timestamp":1622162683000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-020-00563-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,5,28]]},"references-count":82,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2020,12]]}},"alternative-id":["563"],"URL":"https:\/\/doi.org\/10.1007\/s10009-020-00563-2","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,5,28]]},"assertion":[{"value":"28 May 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}