{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,21]],"date-time":"2026-05-21T19:44:49Z","timestamp":1779392689416,"version":"3.53.1"},"reference-count":134,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2018,1,31]],"date-time":"2018-01-31T00:00:00Z","timestamp":1517356800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["CCF 14-38982, CCF 16-17401"],"award-info":[{"award-number":["CCF 14-38982, CCF 16-17401"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000181","name":"AFOSR","doi-asserted-by":"crossref","award":["FA8750-11-2-0084"],"award-info":[{"award-number":["FA8750-11-2-0084"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Model. Comput. Simul."],"published-print":{"date-parts":[[2018,1,31]]},"abstract":"<jats:p>Interactive, distributed, and embedded systems often behave stochastically, for example, when inputs, message delays, or failures conform to a probability distribution. However, reasoning analytically about the behavior of complex stochastic systems is generally infeasible. While simulations of systems are commonly used in engineering practice, they have not traditionally been used to reason about formal specifications. Statistical model checking (SMC) addresses this weakness by using a simulation-based approach to reason about precise properties specified in a stochastic temporal logic. A specification for a communication system may state that within some time bound, the probability that the number of messages in a queue will be greater than 5 must be less than 0.01. Using SMC, executions of a stochastic system are first sampled, after which statistical techniques are applied to determine whether such a property holds. While the output of sample-based methods are not always correct, statistical inference can quantify the confidence in the result produced. In effect, SMC provides a more widely applicable and scalable alternative to analysis of properties of stochastic systems using numerical and symbolic methods. SMC techniques have been successfully applied to analyze systems with large state spaces in areas such as computer networking, security, and systems biology. In this article, we survey SMC algorithms, techniques, and tools, while emphasizing current limitations and tradeoffs between precision and scalability.<\/jats:p>","DOI":"10.1145\/3158668","type":"journal-article","created":{"date-parts":[[2018,2,1]],"date-time":"2018-02-01T13:10:52Z","timestamp":1517490652000},"page":"1-39","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":248,"title":["A Survey of Statistical Model Checking"],"prefix":"10.1145","volume":"28","author":[{"given":"Gul","family":"Agha","sequence":"first","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Karl","family":"Palmskog","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2018,1,31]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.3166\/ejc.16.624-641"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1111\/1467-9884.00082"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40663-8_1"},{"key":"e_1_2_1_4_1","volume-title":"Proceedings of the International Workshop on Foundations of Computer Security (PCS\u201905)","author":"Agha Gul","year":"2005","unstructured":"Gul Agha , Carl Gunter , Michael Greenwald , Sanjeev Khanna , Jos\u00e9 Meseguer , Koushik Sen , and Prasanna Thati . 2005 . Formal modeling and analysis of DoS using probabilistic rewrite theories . In Proceedings of the International Workshop on Foundations of Computer Security (PCS\u201905) . Gul Agha, Carl Gunter, Michael Greenwald, Sanjeev Khanna, Jos\u00e9 Meseguer, Koushik Sen, and Prasanna Thati. 2005. Formal modeling and analysis of DoS using probabilistic rewrite theories. In Proceedings of the International Workshop on Foundations of Computer Security (PCS\u201905)."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.10.040"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/2040096.2040127"},{"key":"e_1_2_1_7_1","unstructured":"APMC. 2005. APMC2 tool. Retrieved from http:\/\/berbiqui.org\/apmc2\/apmc-2.0.0.tar.gz.  APMC. 2005. APMC2 tool. Retrieved from http:\/\/berbiqui.org\/apmc2\/apmc-2.0.0.tar.gz."},{"key":"e_1_2_1_8_1","unstructured":"APMCBeta. 2014. APMC3 Beta tool. Retrieved from https:\/\/web.archive.org\/web\/20140928144328http:\/\/sylvain.berbiqui.org\/apmc.  APMCBeta. 2014. APMC3 Beta tool. Retrieved from https:\/\/web.archive.org\/web\/20140928144328http:\/\/sylvain.berbiqui.org\/apmc."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/3021426.3021438"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/647765.735993"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/343369.343402"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1530873.1530876"},{"key":"e_1_2_1_13_1","unstructured":"Francis Bacon. 1902. Novum Organum. P. F. Collier 8 Sons.  Francis Bacon. 1902. Novum Organum. P. F. Collier 8 Sons."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2003.1205180"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.peva.2015.04.003"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_23"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10373-5_17"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/2429759.2430158"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/2022067.2022071"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28540-0_20"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-45231-8_13"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2006.104"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2008.36"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/1146068.1711154"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40196-1_12"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.85.1"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.05.027"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-13414-2_9"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/HASE.2017.10"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1080\/07362990601139628"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-45943-1_9"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1214\/aoms\/1177700156"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-88562-7_18"},{"key":"e_1_2_1_35_1","volume-title":"Proceedings of the 9th International Symposium on Automated Technology for Verification and Analysis (ATVA\u201911)","author":"Edmund","unstructured":"Edmund M. Clarke and Paolo Zuliani. 2011. Statistical model checking for cyber-physical systems . In Proceedings of the 9th International Symposium on Automated Technology for Verification and Analysis (ATVA\u201911) , Tevfik Bultan and Pao-Ann Hsiung (Eds.). Springer, Berlin, Germany, 1--12. Edmund M. Clarke and Paolo Zuliani. 2011. Statistical model checking for cyber-physical systems. In Proceedings of the 9th International Symposium on Automated Technology for Verification and Analysis (ATVA\u201911), Tevfik Bultan and Pao-Ann Hsiung (Eds.). Springer, Berlin, Germany, 1--12."},{"key":"e_1_2_1_36_1","unstructured":"COSMOS. 2015. COSMOS tool. Retrieved from http:\/\/www.lsv.ens-cachan.fr\/Software\/cosmos\/.  COSMOS. 2015. COSMOS tool. Retrieved from http:\/\/www.lsv.ens-cachan.fr\/Software\/cosmos\/."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_7"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-015-0383-0"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.92.9"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACSD.2014.21"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.5555\/2044973.2044982"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032305.2032332"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.04.012"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04761-9_11"},{"key":"e_1_2_1_45_1","unstructured":"GreatSPN. 2012. GreatSPN tool. Retrieved from http:\/\/www.di.unito.it\/greatspn\/index.html.  GreatSPN. 2012. GreatSPN tool. Retrieved from http:\/\/www.di.unito.it\/greatspn\/index.html."},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_18"},{"key":"e_1_2_1_47_1","volume-title":"Proceedings of the 31st Conference on Uncertainty in Artificial Intelligence, Marina Meila and Tom Heskes (Eds.). AUAI Press","author":"Hadjis Stefan","year":"2015","unstructured":"Stefan Hadjis and Stefano Ermon . 2015 . Importance sampling over sets: A new probabilistic inference scheme . In Proceedings of the 31st Conference on Uncertainty in Artificial Intelligence, Marina Meila and Tom Heskes (Eds.). AUAI Press , Corvallis, OR, 355--364. Retrieved from http:\/\/auai.org\/uai 2015\/proceedings\/papers\/143.pdf. Stefan Hadjis and Stefano Ermon. 2015. Importance sampling over sets: A new probabilistic inference scheme. In Proceedings of the 31st Conference on Uncertainty in Artificial Intelligence, Marina Meila and Tom Heskes (Eds.). AUAI Press, Corvallis, OR, 355--364. Retrieved from http:\/\/auai.org\/uai2015\/proceedings\/papers\/143.pdf."},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211866"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.5555\/646486.694486"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.5555\/829525.831103"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38697-8_21"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/1839764.1839776"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2012.19"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24622-0_8"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2006.5"},{"key":"e_1_2_1_56_1","volume-title":"Proceedings of the 3rd International Workshop on the Numerical Solution of Markov Chains. 188--207","author":"Hermanns Holger","year":"1999","unstructured":"Holger Hermanns , Joachim Meyer-Kayser , and Markus Siegle . 1999 . Multi terminal binary decision diagrams to represent and analyse continuous time markov chains . In Proceedings of the 3rd International Workshop on the Numerical Solution of Markov Chains. 188--207 . Holger Hermanns, Joachim Meyer-Kayser, and Markus Siegle. 1999. Multi terminal binary decision diagrams to represent and analyse continuous time markov chains. In Proceedings of the 3rd International Workshop on the Numerical Solution of Markov Chains. 188--207."},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1080\/01621459.1963.10500830"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_24"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1109\/49.62852"},{"key":"e_1_2_1_60_1","volume-title":"Measurement, Simulation, and Modeling","author":"Jain Raj","unstructured":"Raj Jain . 1991. The Art of Computer Systems Performance Analysis: Techniques for Experimental Design , Measurement, Simulation, and Modeling . Wiley , Hoboken, NJ . Raj Jain. 1991. The Art of Computer Systems Performance Analysis: Techniques for Experimental Design, Measurement, Simulation, and Modeling. Wiley, Hoboken, NJ."},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.5555\/1787497.1787510"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_38"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-45231-8_11"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2016.08.009"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03845-7_15"},{"key":"e_1_2_1_66_1","volume-title":"Exploring behaviors of stochastic differential equation models of biological systems using change of measures. BMC Bioinfo. 13, 5 (12","author":"Jha Sumit Kumar","year":"2012","unstructured":"Sumit Kumar Jha and Christopher James Langmead . 2012. Exploring behaviors of stochastic differential equation models of biological systems using change of measures. BMC Bioinfo. 13, 5 (12 Apr 2012 ), S8. Sumit Kumar Jha and Christopher James Langmead. 2012. Exploring behaviors of stochastic differential equation models of biological systems using change of measures. BMC Bioinfo. 13, 5 (12 Apr 2012), S8."},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-47166-2_4"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2010.35"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032305.2032352"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2010.80"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/2489253.2489256"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-23820-3_17"},{"key":"e_1_2_1_73_1","first-page":"303","article-title":"Sequential analysis: Some classical problems and new challenges","volume":"11","author":"Lai Tze Leung","year":"2001","unstructured":"Tze Leung Lai . 2001 . Sequential analysis: Some classical problems and new challenges . Statistica Sinica 11 , 2 (2001), 303 -- 351 . Tze Leung Lai. 2001. Sequential analysis: Some classical problems and new challenges. Statistica Sinica 11, 2 (2001), 303--351.","journal-title":"Statistica Sinica"},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90030-6"},{"key":"e_1_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.5555\/645777.668441"},{"key":"e_1_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2007.11.006"},{"key":"e_1_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-014-0344-z"},{"key":"e_1_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1145\/1225275.1225280"},{"key":"e_1_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-15201-1_23"},{"key":"e_1_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-45994-3_2"},{"key":"e_1_2_1_81_1","volume-title":"Transactions on Foundations for Mastering Change I","author":"Legay Axel","unstructured":"Axel Legay and Louis-Marie Traonouez . 2016. Statistical model checking with change detection . In Transactions on Foundations for Mastering Change I , Bernhard Steffen (Ed.). Springer International Publishing , Cham, 157--179. Axel Legay and Louis-Marie Traonouez. 2016. Statistical model checking with change detection. In Transactions on Foundations for Mastering Change I, Bernhard Steffen (Ed.). Springer International Publishing, Cham, 157--179."},{"key":"e_1_2_1_82_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_2_1_83_1","doi-asserted-by":"publisher","DOI":"10.1111\/1467-9884.00068"},{"key":"e_1_2_1_84_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22264-6_15"},{"key":"e_1_2_1_85_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54580-5_17"},{"key":"e_1_2_1_86_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-46982-9_1"},{"key":"e_1_2_1_87_1","unstructured":"MARCIE. 2017. MARCIE tool. Retrieved from http:\/\/www-dssz.informatik.tu-cottbus.de\/DSSZ\/Software\/Marcie.  MARCIE. 2017. MARCIE tool. Retrieved from http:\/\/www-dssz.informatik.tu-cottbus.de\/DSSZ\/Software\/Marcie."},{"key":"e_1_2_1_88_1","doi-asserted-by":"publisher","DOI":"10.5555\/2075089.2075103"},{"key":"e_1_2_1_89_1","doi-asserted-by":"publisher","DOI":"10.1007\/11730637_35"},{"key":"e_1_2_1_90_1","unstructured":"MODES. 2006. MODES tool. Retrieved from http:\/\/www.modestchecker.net.  MODES. 2006. MODES tool. Retrieved from http:\/\/www.modestchecker.net."},{"key":"e_1_2_1_91_1","unstructured":"MRMC. 2011. MRMC tool. Retrieved from http:\/\/www.mrmc-tool.org.  MRMC. 2011. MRMC tool. Retrieved from http:\/\/www.mrmc-tool.org."},{"key":"e_1_2_1_92_1","unstructured":"MultiVESTA. 2015. MultiVESTA tool. Retrieved from http:\/\/sysma.imtlucca.it\/tools\/multivesta\/.  MultiVESTA. 2015. MultiVESTA tool. Retrieved from http:\/\/sysma.imtlucca.it\/tools\/multivesta\/."},{"key":"e_1_2_1_93_1","unstructured":"NIST. 2017. NIST\/SEMATECH e-Handbook of Statistical Methods. Retrieved from http:\/\/www.itl.nist.gov\/div898\/handbook\/ppc\/section3\/ppc333.htm.  NIST. 2017. NIST\/SEMATECH e-Handbook of Statistical Methods. Retrieved from http:\/\/www.itl.nist.gov\/div898\/handbook\/ppc\/section3\/ppc333.htm."},{"key":"e_1_2_1_94_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-014-0313-6"},{"key":"e_1_2_1_95_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40708-6_10"},{"key":"e_1_2_1_96_1","doi-asserted-by":"publisher","DOI":"10.1145\/2601381.2601394"},{"key":"e_1_2_1_97_1","doi-asserted-by":"publisher","DOI":"10.1080\/00401706.1967.10490457"},{"key":"e_1_2_1_98_1","unstructured":"PLASMA. 2015. PLASMA Lab. Retrieved from http:\/\/project.inria.fr\/plasma-lab\/.  PLASMA. 2015. PLASMA Lab. Retrieved from http:\/\/project.inria.fr\/plasma-lab\/."},{"key":"e_1_2_1_99_1","volume-title":"Conjectures and Refutations: The Growth of Scientific Knowledge","author":"Popper Karl","unstructured":"Karl Popper . 1968. Conjectures and Refutations: The Growth of Scientific Knowledge . Harper Torchbooks . Karl Popper. 1968. Conjectures and Refutations: The Growth of Scientific Knowledge. Harper Torchbooks."},{"key":"e_1_2_1_100_1","unstructured":"PRISM. 2017. PRISM Statistical Model Checker. Retrieved from http:\/\/www.prismmodelchecker.org\/manual\/RunningPRISM\/StatisticalModelChecking.  PRISM. 2017. PRISM Statistical Model Checker. Retrieved from http:\/\/www.prismmodelchecker.org\/manual\/RunningPRISM\/StatisticalModelChecking."},{"key":"e_1_2_1_101_1","doi-asserted-by":"publisher","DOI":"10.5555\/235610.235641"},{"key":"e_1_2_1_102_1","unstructured":"PVESTA. 2011. PVESTA tool. Retrieved from http:\/\/maude.cs.uiuc.edu\/tools\/pvesta\/.  PVESTA. 2011. PVESTA tool. Retrieved from http:\/\/maude.cs.uiuc.edu\/tools\/pvesta\/."},{"key":"e_1_2_1_103_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-47166-2_56"},{"key":"e_1_2_1_104_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2010.39"},{"key":"e_1_2_1_105_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-015-0368-z"},{"key":"e_1_2_1_106_1","volume-title":"SAM: Stochastic Analyser for Mobility.","author":"SAM.","year":"2010","unstructured":"SAM. 2010 . SAM: Stochastic Analyser for Mobility. Retrieved from http:\/\/rap.dsi.unifi.it\/SAM\/. SAM. 2010. SAM: Stochastic Analyser for Mobility. Retrieved from http:\/\/rap.dsi.unifi.it\/SAM\/."},{"key":"e_1_2_1_107_1","doi-asserted-by":"publisher","DOI":"10.5555\/2958368.2958389"},{"key":"e_1_2_1_108_1","unstructured":"SBIP. 2013. SBIP tool. Retrieved from http:\/\/www-verimag.imag.fr\/Statistical-Model-Checking.html.  SBIP. 2013. SBIP tool. Retrieved from http:\/\/www-verimag.imag.fr\/Statistical-Model-Checking.html."},{"key":"e_1_2_1_109_1","doi-asserted-by":"publisher","DOI":"10.4108\/icst.valuetools.2013.254377"},{"key":"e_1_2_1_110_1","doi-asserted-by":"publisher","DOI":"10.5555\/998675.999446"},{"key":"e_1_2_1_111_1","series-title":"Lecture Notes in Computer Science","volume-title":"Statistical model checking of black-box probabilistic systems","author":"Sen Koushik","unstructured":"Koushik Sen , Mahesh Viswanathan , and Gul Agha . 2004. Statistical model checking of black-box probabilistic systems . In Computer Aided Verification, Rajeev Alur and Doron A. Peled (Eds.). Lecture Notes in Computer Science , Vol. 3114 . Springer , Berlin, Germany , 202--215. Koushik Sen, Mahesh Viswanathan, and Gul Agha. 2004. Statistical model checking of black-box probabilistic systems. In Computer Aided Verification, Rajeev Alur and Doron A. Peled (Eds.). Lecture Notes in Computer Science, Vol. 3114. Springer, Berlin, Germany, 202--215."},{"key":"e_1_2_1_112_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_26"},{"key":"e_1_2_1_113_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2005.42"},{"key":"e_1_2_1_114_1","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_26"},{"key":"e_1_2_1_115_1","doi-asserted-by":"crossref","unstructured":"Rajan Srinivasan. 2002. Importance Sampling. Springer Berlin Germany.  Rajan Srinivasan. 2002. Importance Sampling. Springer Berlin Germany.","DOI":"10.1007\/978-3-662-05052-1"},{"key":"e_1_2_1_116_1","doi-asserted-by":"publisher","DOI":"10.1198\/000313007X222488"},{"key":"e_1_2_1_117_1","doi-asserted-by":"publisher","DOI":"10.1201\/b17279"},{"key":"e_1_2_1_118_1","volume-title":"Proceedings of the 31st AAAI Conference on Artificial Intelligence (AAAI\u201917)","author":"Philip","unstructured":"Philip S. Thomas and Emma Brunskill. 2017. Importance sampling with unequal support . In Proceedings of the 31st AAAI Conference on Artificial Intelligence (AAAI\u201917) . AAAI Press, Palo Alto, CA. Retrieved from https:\/\/aaai.org\/ocs\/index.php\/AAAI\/AAAI17\/paper\/view\/14957\/14457. Philip S. Thomas and Emma Brunskill. 2017. Importance sampling with unequal support. In Proceedings of the 31st AAAI Conference on Artificial Intelligence (AAAI\u201917). AAAI Press, Palo Alto, CA. Retrieved from https:\/\/aaai.org\/ocs\/index.php\/AAAI\/AAAI17\/paper\/view\/14957\/14457."},{"key":"e_1_2_1_119_1","volume-title":"Queuing And Computer Science Applications","author":"Trivedi Kishor S.","unstructured":"Kishor S. Trivedi . 2008. Probability 8 Statistics With Reliability , Queuing And Computer Science Applications ( 2 nd ed.). Wiley, Hoboken , NJ. Kishor S. Trivedi. 2008. Probability 8 Statistics With Reliability, Queuing And Computer Science Applications (2nd ed.). Wiley, Hoboken, NJ.","edition":"2"},{"key":"e_1_2_1_120_1","unstructured":"UPPAAL 2015. UPPAAL. Retrieved from http:\/\/www.uppaal.org.  UPPAAL 2015. UPPAAL. Retrieved from http:\/\/www.uppaal.org."},{"key":"e_1_2_1_121_1","doi-asserted-by":"publisher","DOI":"10.1214\/aoms\/1177731118"},{"key":"e_1_2_1_122_1","volume-title":"Statistical Decision Functions","author":"Wald Abraham","unstructured":"Abraham Wald . 1950. Statistical Decision Functions . Wiley , New York, NY . Abraham Wald. 1950. Statistical Decision Functions. Wiley, New York, NY."},{"key":"e_1_2_1_123_1","volume-title":"Breakthroughs in Statistics: Foundations and Basic Theory","author":"Wald Abraham","unstructured":"Abraham Wald . 1992. Breakthroughs in Statistics: Foundations and Basic Theory . Springer New York , New York, NY , Chapter Sequential Tests of Statistical Hypotheses, 256--298. Abraham Wald. 1992. Breakthroughs in Statistics: Foundations and Basic Theory. Springer New York, New York, NY, Chapter Sequential Tests of Statistical Hypotheses, 256--298."},{"key":"e_1_2_1_124_1","doi-asserted-by":"publisher","DOI":"10.1057\/jors.1993.181"},{"key":"e_1_2_1_125_1","unstructured":"Ymer. 2015. Ymer tool. Retrieved from http:\/\/www.tempastic.org\/ymer\/.  Ymer. 2015. Ymer tool. Retrieved from http:\/\/www.tempastic.org\/ymer\/."},{"key":"e_1_2_1_126_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_25"},{"key":"e_1_2_1_127_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_43"},{"key":"e_1_2_1_128_1","doi-asserted-by":"publisher","DOI":"10.1007\/11609773_10"},{"key":"e_1_2_1_129_1","doi-asserted-by":"publisher","DOI":"10.5555\/1987100.1987110"},{"key":"e_1_2_1_130_1","doi-asserted-by":"publisher","DOI":"10.5555\/3220880.3220972"},{"key":"e_1_2_1_131_1","volume-title":"Simmons","author":"Younes H\u00e5kan L. S.","year":"2002","unstructured":"H\u00e5kan L. S. Younes and Reid G . Simmons . 2002 . Probabilistic verification of discrete event systems using acceptance sampling. In Computer Aided Verification, Ed Brinksma and Kim Guldstrand Larsen (Eds.). Lecture Notes in Computer Science, Vol. 2404 . Springer , Berlin, Germany, 223--235. H\u00e5kan L. S. Younes and Reid G. Simmons. 2002. Probabilistic verification of discrete event systems using acceptance sampling. In Computer Aided Verification, Ed Brinksma and Kim Guldstrand Larsen (Eds.). Lecture Notes in Computer Science, Vol. 2404. Springer, Berlin, Germany, 223--235."},{"key":"e_1_2_1_132_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2006.05.002"},{"key":"e_1_2_1_133_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-014-0343-0"},{"key":"e_1_2_1_134_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-013-0195-3"}],"container-title":["ACM Transactions on Modeling and Computer Simulation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158668","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3158668","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3158668","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:26:10Z","timestamp":1750213570000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158668"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,1,31]]},"references-count":134,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2018,1,31]]}},"alternative-id":["10.1145\/3158668"],"URL":"https:\/\/doi.org\/10.1145\/3158668","relation":{},"ISSN":["1049-3301","1558-1195"],"issn-type":[{"value":"1049-3301","type":"print"},{"value":"1558-1195","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,1,31]]},"assertion":[{"value":"2017-02-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-11-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-01-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}