{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,18]],"date-time":"2026-06-18T05:56:55Z","timestamp":1781762215271,"version":"3.54.5"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319663340","type":"print"},{"value":"9783319663357","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-66335-7_24","type":"book-chapter","created":{"date-parts":[[2017,8,9]],"date-time":"2017-08-09T23:53:48Z","timestamp":1502322828000},"page":"351-367","source":"Crossref","is-referenced-by-count":6,"title":["Multilevel Monte Carlo Method for Statistical Model Checking of Hybrid Systems"],"prefix":"10.1007","author":[{"given":"Sadegh","family":"Esmaeil Zadeh Soudjani","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rupak","family":"Majumdar","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Tigran","family":"Nagapetyan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2017,8,11]]},"reference":[{"issue":"11","key":"24_CR1","doi-asserted-by":"crossref","first-page":"2724","DOI":"10.1016\/j.automatica.2008.03.027","volume":"44","author":"A Abate","year":"2008","unstructured":"Abate, A., Prandini, M., Lygeros, J., Sastry, S.: Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems. Automatica 44(11), 2724\u20132734 (2008)","journal-title":"Automatica"},{"issue":"6","key":"24_CR2","doi-asserted-by":"crossref","first-page":"524","DOI":"10.1109\/TSE.2003.1205180","volume":"29","author":"C Baier","year":"2003","unstructured":"Baier, C., Haverkort, B., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for continuous-time Markov chains. Trans. Softw. Eng. 29(6), 524\u2013541 (2003)","journal-title":"Trans. Softw. Eng."},{"key":"24_CR3","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"24_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/3-540-36580-X_12","volume-title":"Hybrid Systems: Computation and Control","author":"ML Bujorianu","year":"2003","unstructured":"Bujorianu, M.L., Lygeros, J.: Reachability questions in piecewise deterministic Markov processes. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol. 2623, pp. 126\u2013140. Springer, Heidelberg (2003). doi: 10.1007\/3-540-36580-X_12"},{"key":"24_CR5","doi-asserted-by":"crossref","unstructured":"Bujorianu, M.L., Lygeros, J.: General stochastic hybrid systems: modelling and optimal control. In: Proceedings of 43rd IEEE Conference Decision Control, pp. 1872\u20131877 (2004)","DOI":"10.1109\/CDC.2004.1430320"},{"key":"24_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1007\/978-3-642-28891-3_39","volume-title":"NASA Formal Methods","author":"P Bulychev","year":"2012","unstructured":"Bulychev, P., David, A., Larsen, K.G., Legay, A., Miku\u010dionis, M., Poulsen, D.B.: Checking and distributing statistical model checking. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 449\u2013463. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-28891-3_39"},{"key":"24_CR7","doi-asserted-by":"crossref","unstructured":"Cassandras, C.G., Lygeros, J. (eds.) Stochastic Hybrid Systems. Control Engineering, vol. 24. CRC Press, Boca Raton (2006)","DOI":"10.1201\/9781420008548"},{"key":"24_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-24372-1_1","volume-title":"Automated Technology for Verification and Analysis","author":"EM Clarke","year":"2011","unstructured":"Clarke, E.M., Zuliani, P.: Statistical model checking for cyber-physical systems. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 1\u201312. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-24372-1_1"},{"key":"24_CR9","doi-asserted-by":"crossref","unstructured":"Daca, P., Henzinger, T.A., K\u0159et\u00ednsk\u00fd, J., Petrov, T.: Faster statistical model checking for unbounded temporal properties. ACM Trans. Comput. Logic 18(2), 12:1\u201312:25 (2017)","DOI":"10.1145\/3060139"},{"key":"24_CR10","unstructured":"Esmaeil Zadeh Soudjani, S.: Formal abstractions for automated verification and synthesis of stochastic systems. Ph.D. thesis, Delft, NL, November 2014"},{"issue":"2","key":"24_CR11","doi-asserted-by":"crossref","first-page":"921","DOI":"10.1137\/120871456","volume":"12","author":"S Esmaeil Zadeh Soudjani","year":"2013","unstructured":"Esmaeil Zadeh Soudjani, S., Abate, A.: Adaptive and sequential gridding procedures for the abstraction and verification of stochastic processes. SIAM J. Appl. Dyn. Syst. 12(2), 921\u2013956 (2013)","journal-title":"SIAM J. Appl. Dyn. Syst."},{"issue":"3","key":"24_CR12","doi-asserted-by":"crossref","first-page":"975","DOI":"10.1109\/TCST.2014.2358844","volume":"23","author":"S Esmaeil Zadeh Soudjani","year":"2015","unstructured":"Esmaeil Zadeh Soudjani, S., Abate, A.: Aggregation and control of populations of thermostatically controlled loads by formal abstractions. IEEE Trans. Control Syst. Technol. 23(3), 975\u2013990 (2015)","journal-title":"IEEE Trans. Control Syst. Technol."},{"key":"24_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/978-3-319-10696-0_6","volume-title":"Quantitative Evaluation of Systems","author":"S Esmaeil Zadeh Soudjani","year":"2014","unstructured":"Esmaeil Zadeh Soudjani, S., Gerwinn, S., Ellen, C., Fr\u00e4nzle, M., Abate, A.: Formal synthesis and validation of inhomogeneous thermostatically controlled loads. In: Norman, G., Sanders, W. (eds.) QEST 2014. LNCS, vol. 8657, pp. 57\u201373. Springer, Cham (2014). doi: 10.1007\/978-3-319-10696-0_6"},{"key":"24_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-662-49674-9_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Esmaeil Zadeh Soudjani","year":"2016","unstructured":"Esmaeil Zadeh Soudjani, S., Majumdar, R., Abate, A.: Safety verification of continuous-space pure jump Markov processes. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 147\u2013163. Springer, Heidelberg (2016). doi: 10.1007\/978-3-662-49674-9_9"},{"key":"24_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/978-3-540-78929-1_13","volume-title":"Hybrid Systems: Computation and Control","author":"M Fr\u00e4nzle","year":"2008","unstructured":"Fr\u00e4nzle, M., Hermanns, H., Teige, T.: Stochastic satisfiability modulo theory: a novel technique for the analysis of probabilistic hybrid systems. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol. 4981, pp. 172\u2013186. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-78929-1_13"},{"key":"24_CR16","unstructured":"Giles, M.B., Nagapetyan, T., Ritter, K.: Adaptive Multilevel Monte Carlo Approximation of Distribution Functions. ArXiv e-prints, June 2017"},{"issue":"3","key":"24_CR17","doi-asserted-by":"crossref","first-page":"607","DOI":"10.1287\/opre.1070.0496","volume":"56","author":"MB Giles","year":"2008","unstructured":"Giles, M.B.: Multilevel Monte Carlo path simulation. Oper. Res. 56(3), 607\u2013617 (2008)","journal-title":"Oper. Res."},{"key":"24_CR18","doi-asserted-by":"crossref","first-page":"259","DOI":"10.1017\/S096249291500001X","volume":"24","author":"MB Giles","year":"2015","unstructured":"Giles, M.B.: Multilevel Monte Carlo methods. Acta Numer. 24, 259\u2013328 (2015)","journal-title":"Acta Numer."},{"issue":"1","key":"24_CR19","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1137\/140960086","volume":"3","author":"MB Giles","year":"2015","unstructured":"Giles, M.B., Nagapetyan, T., Ritter, K.: Multilevel Monte Carlo approximation of distribution functions and densities. SIAM\/ASA J. Uncertain. Quantif. 3(1), 267\u2013295 (2015)","journal-title":"SIAM\/ASA J. Uncertain. Quantif."},{"issue":"2","key":"24_CR20","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1006\/jcom.1998.0471","volume":"14","author":"S Heinrich","year":"1998","unstructured":"Heinrich, S.: Monte Carlo complexity of global solution of integral equations. J. Complexity 14(2), 151\u2013175 (1998)","journal-title":"J. Complexity"},{"key":"24_CR21","doi-asserted-by":"crossref","unstructured":"Kamgarpour, M., Ellen, C., Esmaeil Zadeh Soudjani, S., Gerwinn, S., Mathieu, J.L., Mullner, N., Abate, A., Callaway, D.S., Fr\u00e4nzle, M., Lygeros, J.: Modeling options for demand side participation of thermostatically controlled loads. In: International Conference on Bulk Power System Dynamics and Control, pp. 1\u201315, August 2013","DOI":"10.1109\/IREP.2013.6629396"},{"key":"24_CR22","doi-asserted-by":"crossref","unstructured":"K\u0159et\u00ednsk\u00fd, J.: Survey of statistical verification of linear unbounded properties: model checking and distances, pp. 27\u201345. Springer, Cham (2016)","DOI":"10.1007\/978-3-319-47166-2_3"},{"key":"24_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-662-45231-8_10","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications","author":"KG Larsen","year":"2014","unstructured":"Larsen, K.G., Legay, A.: Statistical model checking past, present, and future. In: Margaria, T., Steffen, B. (eds.) ISoLA 2014. LNCS, vol. 8803, pp. 135\u2013142. Springer, Heidelberg (2014). doi: 10.1007\/978-3-662-45231-8_10"},{"key":"24_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-642-16612-9_11","volume-title":"Runtime Verification","author":"A Legay","year":"2010","unstructured":"Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: an overview. In: Barringer, H., et al. (eds.) RV 2010. LNCS, vol. 6418, pp. 122\u2013135. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-16612-9_11"},{"issue":"1","key":"24_CR25","doi-asserted-by":"crossref","first-page":"430","DOI":"10.1109\/TPWRS.2012.2204074","volume":"28","author":"JL Mathieu","year":"2013","unstructured":"Mathieu, J.L., Koch, S., Callaway, D.S.: State estimation and control of electric loads to manage real-time energy imbalance. IEEE Trans. Power Syst. 28(1), 430\u2013440 (2013)","journal-title":"IEEE Trans. Power Syst."},{"key":"24_CR26","doi-asserted-by":"crossref","unstructured":"Pola, G., Bujorianu, M.L., Lygeros, J., Di Benedetto, M.D.: Stochastic hybrid models: an overview. In: Analysis and Design of Hybrid Systems (2003)","DOI":"10.1016\/S1474-6670(17)36405-4"},{"issue":"8","key":"24_CR27","doi-asserted-by":"crossref","first-page":"1415","DOI":"10.1109\/TAC.2007.902736","volume":"52","author":"S Prajna","year":"2007","unstructured":"Prajna, S., Jadbabaie, A., Pappas, G.J.: A framework for worst-case and stochastic safety verification using barrier certificates. IEEE Trans. Autom. Control 52(8), 1415\u20131428 (2007)","journal-title":"IEEE Trans. Autom. Control"},{"key":"24_CR28","doi-asserted-by":"crossref","unstructured":"Tkachev, I., Mereacre, A., Katoen, J.-P., Abate, A.: Quantitative automata-based controller synthesis for non-autonomous stochastic hybrid systems. In: Hybrid Systems: Computation and Control, pp. 293\u2013302. ACM, New York (2013)","DOI":"10.1145\/2461328.2461373"},{"key":"24_CR29","doi-asserted-by":"crossref","unstructured":"Wang, Y., Roohi, N., West, M., Viswanathan, M., Dullerud, G.E.: Statistical verification of dynamical systems using set oriented methods. In: Hybrid Systems: Computation and Control, pp. 169\u2013178. ACM, New York (2015)","DOI":"10.1145\/2728606.2728627"}],"container-title":["Lecture Notes in Computer Science","Quantitative Evaluation of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66335-7_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,2]],"date-time":"2019-10-02T02:39:04Z","timestamp":1569983944000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66335-7_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319663340","9783319663357"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66335-7_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}