{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,18]],"date-time":"2026-08-18T14:15:51Z","timestamp":1787062551324,"version":"3.56.0"},"reference-count":29,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2019,10,31]],"date-time":"2019-10-31T00:00:00Z","timestamp":1572480000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Model. Comput. Simul."],"published-print":{"date-parts":[[2019,10,31]]},"abstract":"<jats:p>\n                    Statistical Model Checking (SMC) is an approximate verification method that overcomes the state space explosion problem for probabilistic systems by Monte Carlo simulations. Simulations might, however, be costly if many samples are required. It is thus necessary to implement efficient algorithms to reduce the sample size while preserving precision and accuracy. In the literature, some sequential schemes have been provided for the estimation of property occurrence based on predefined confidence and\n                    <jats:italic>absolute<\/jats:italic>\n                    or\n                    <jats:italic>relative<\/jats:italic>\n                    error. Nevertheless, these algorithms remain conservative and may result in huge sample sizes if the required precision standards are demanding. In this article, we compare some useful bounds and some sequential methods. We propose outperforming and rigorous alternative schemes based on Massart bounds and robust confidence intervals. Our theoretical and empirical analyses show that our proposal reduces the sample size while providing the required guarantees on error bounds.\n                  <\/jats:p>","DOI":"10.1145\/3310226","type":"journal-article","created":{"date-parts":[[2019,11,18]],"date-time":"2019-11-18T08:01:53Z","timestamp":1574064113000},"page":"1-22","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Sequential Schemes for Frequentist Estimation of Properties in Statistical Model Checking"],"prefix":"10.1145","volume":"29","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2770-8394","authenticated-orcid":false,"given":"Cyrille","family":"Jegourel","sequence":"first","affiliation":[{"name":"Singapore University of Technology and Design, Singapore, Singapore"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jun","family":"Sun","sequence":"additional","affiliation":[{"name":"Singapore University of Technology and Design, Singapore, Singapore"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jin Song","family":"Dong","sequence":"additional","affiliation":[{"name":"University of Griffith, Queensland, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,11,18]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158668"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(79)90045-X"},{"key":"e_1_2_1_3_1","volume-title":"HASL: A new approach for performance evaluation and model checking from concepts to experimentation. Perf. Eval. 90 (Aug.","author":"Ballarini Paolo","year":"2015"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1214\/ss\/1009213286"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/WI-IAT.2013.3"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1214\/aoms\/1177729330"},{"key":"e_1_2_1_7_1","volume-title":"Proceedings of the ATVA. 1--12","author":"Clarke E."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1093\/biomet\/26.4.404"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539797315306"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-014-0361-y"},{"key":"e_1_2_1_11_1","volume-title":"Probabilistic Methods in Combinatorics","author":"Erd\u0151s Paul"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1198\/tast.2010.09140"},{"key":"e_1_2_1_13_1","volume-title":"Proceedings of the ISoLA. 223--238","author":"Grosu R."},{"key":"e_1_2_1_14_1","volume-title":"Proceedings of the VMCAI, Bernhard Steffen and Giorgio Levi (Eds.). LNCS","volume":"2937","author":"H\u00e9rault T."},{"key":"e_1_2_1_15_1","volume-title":"Proceedings of the QEST. 129--130","author":"H\u00e9rault T."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1080\/01621459.1963.10500830"},{"key":"e_1_2_1_17_1","volume-title":"Proceedings of the TACAS. 498--503","author":"J\u00e9gourel C."},{"key":"e_1_2_1_18_1","first-page":"576","article-title":"Importance splitting for statistical model checking rare properties","volume":"8044","author":"Jegourel C.","year":"2013","journal-title":"Proceedings of the CAV. LNCS"},{"key":"e_1_2_1_19_1","volume-title":"Proceedings of the ISoLA. 27--45","author":"Kret\u00ednsk\u00fd Jan","year":"2016"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2004.1348048"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-7152(01)00029-3"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1214\/aop\/1176990746"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1080\/01621459.1949.10483310"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02883985"},{"key":"e_1_2_1_25_1","volume-title":"Introduction to Probability and Statistics for Engineers and Scientists","author":"Ross Sheldon M.","edition":"5"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1214\/aoms\/1177731118"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.09.003"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_4"},{"key":"e_1_2_1_30_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\/3310226","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3310226","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:13:16Z","timestamp":1750198396000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3310226"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10,31]]},"references-count":29,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2019,10,31]]}},"alternative-id":["10.1145\/3310226"],"URL":"https:\/\/doi.org\/10.1145\/3310226","relation":{},"ISSN":["1049-3301","1558-1195"],"issn-type":[{"value":"1049-3301","type":"print"},{"value":"1558-1195","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,10,31]]},"assertion":[{"value":"2018-01-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-01-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-11-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}