{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,16]],"date-time":"2026-05-16T06:50:16Z","timestamp":1778914216386,"version":"3.51.4"},"reference-count":52,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2013,8,27]],"date-time":"2013-08-27T00:00:00Z","timestamp":1377561600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2013,10]]},"DOI":"10.1007\/s10703-013-0195-3","type":"journal-article","created":{"date-parts":[[2013,8,26]],"date-time":"2013-08-26T21:12:51Z","timestamp":1377551571000},"page":"338-367","source":"Crossref","is-referenced-by-count":77,"title":["Bayesian statistical model checking with application to Stateflow\/Simulink verification"],"prefix":"10.1007","volume":"43","author":[{"given":"Paolo","family":"Zuliani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andr\u00e9","family":"Platzer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Edmund M.","family":"Clarke","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2013,8,27]]},"reference":[{"key":"195_CR1","series-title":"LNCS","first-page":"115","volume-title":"ICALP","author":"R Alur","year":"1991","unstructured":"Alur R, Courcoubetis C, Dill D (1991) Model-checking for probabilistic real-time systems. In: ICALP. LNCS, vol 510, pp 115\u2013126"},{"key":"195_CR2","series-title":"LNCS","first-page":"430","volume-title":"ICALP","author":"C Baier","year":"1997","unstructured":"Baier C, Clarke EM, Hartonas-Garmhausen V, Kwiatkowska MZ, Ryan M (1997) Symbolic model checking for probabilistic processes. In: ICALP. LNCS, vol 1256, pp 430\u2013440"},{"issue":"6","key":"195_CR3","doi-asserted-by":"crossref","first-page":"524","DOI":"10.1109\/TSE.2003.1205180","volume":"29","author":"C Baier","year":"2003","unstructured":"Baier C, Haverkort BR, Hermanns H, Katoen J-P (2003) Model-checking algorithms for continuous-time Markov chains. IEEE Trans Softw Eng 29(6):524\u2013541","journal-title":"IEEE Trans Softw Eng"},{"key":"195_CR4","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511762543","volume-title":"Special functions","author":"R Beals","year":"2010","unstructured":"Beals R, Wong R (2010) Special functions. Cambridge University Press, Cambridge"},{"key":"195_CR5","doi-asserted-by":"crossref","first-page":"660","DOI":"10.1080\/01621459.1960.10483366","volume":"55","author":"R Bechhofer","year":"1960","unstructured":"Bechhofer R (1960) A note on the limiting relative efficiency of the Wald sequential probability ratio test. J Am Stat Assoc 55:660\u2013663","journal-title":"J Am Stat Assoc"},{"key":"195_CR6","series-title":"Lecture notes contr inf","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/11587392_1","volume-title":"Stochastic hybrid systems: theory and safety critical applications","author":"ML Bujorianu","year":"2006","unstructured":"Bujorianu ML, Lygeros J (2006) Towards a general theory of stochastic hybrid systems. In: Blom HAP, Lygeros J (eds) Stochastic hybrid systems: theory and safety critical applications. Lecture notes contr inf, vol 337. Springer, Berlin, pp 3\u201330"},{"key":"195_CR7","volume-title":"Bayesian methods for data analysis","author":"BP Carlin","year":"2009","unstructured":"Carlin BP, Louis TA (2009) Bayesian methods for data analysis, 3rd edn. CRC Press, Boca Raton","edition":"3"},{"key":"195_CR8","volume-title":"Stochastic hybrid systems","year":"2006","unstructured":"Cassandras CG, Lygeros J (eds) (2006) Stochastic hybrid systems. CRC Press, Boca Raton"},{"issue":"1","key":"195_CR9","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1838552.1838553","volume":"12","author":"R Chadha","year":"2010","unstructured":"Chadha R, Viswanathan M (2010) A counterexample-guided abstraction-refinement framework for Markov decision processes. ACM Trans Comput Log 12(1):1","journal-title":"ACM Trans Comput Log"},{"issue":"2","key":"195_CR10","doi-asserted-by":"crossref","first-page":"457","DOI":"10.1214\/aoms\/1177700156","volume":"36","author":"YS Chow","year":"1965","unstructured":"Chow YS, Robbins H (1965) On the asymptotic theory of fixed-width sequential confidence intervals for the mean. Ann Math Stat 36(2):457\u2013462","journal-title":"Ann Math Stat"},{"key":"195_CR11","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/978-3-540-24611-4_5","volume-title":"Validation of stochastic systems","author":"F Ciesinski","year":"2004","unstructured":"Ciesinski F, Gr\u00f6\u00dfer M (2004) On probabilistic computation tree logic. In: Validation of stochastic systems. LNCS, vol 2925. Springer, Berlin, pp 147\u2013188"},{"key":"195_CR12","volume-title":"Measure theory","author":"DL Cohn","year":"1994","unstructured":"Cohn DL (1994) Measure theory. Birkh\u00e4user, Basel"},{"issue":"4","key":"195_CR13","doi-asserted-by":"crossref","first-page":"857","DOI":"10.1145\/210332.210339","volume":"42","author":"C Courcoubetis","year":"1995","unstructured":"Courcoubetis C, Yannakakis M (1995) The complexity of probabilistic verification. J ACM 42(4):857\u2013907","journal-title":"J ACM"},{"key":"195_CR14","doi-asserted-by":"crossref","DOI":"10.1002\/0471729000","volume-title":"Optimal statistical decisions","author":"MH DeGroot","year":"2004","unstructured":"DeGroot MH (2004) Optimal statistical decisions. Wiley, New York"},{"key":"195_CR15","first-page":"133","volume-title":"Bayesian statistics 2: 2nd Valencia international meeting","author":"P Diaconis","year":"1985","unstructured":"Diaconis P, Ylvisaker D (1985) Quantifying prior opinion. In: Bayesian statistics 2: 2nd Valencia international meeting. Elsevier, Amsterdam, pp 133\u2013156"},{"key":"195_CR16","series-title":"ENTCS","first-page":"44","volume-title":"Runtime verification (RV\u201901)","author":"B Finkbeiner","year":"2001","unstructured":"Finkbeiner B, Sipma H (2001) Checking finite traces using alternating automata. In: Runtime verification (RV\u201901). ENTCS, vol 55, pp 44\u201360"},{"key":"195_CR17","volume-title":"Bayesian data analysis","author":"A Gelman","year":"1997","unstructured":"Gelman A, Carlin JB, Stern HS, Rubin DB (1997) Bayesian data analysis. Chapman & Hall, London"},{"issue":"6","key":"195_CR18","doi-asserted-by":"crossref","first-page":"1952","DOI":"10.1137\/S0363012996299302","volume":"35","author":"MK Ghosh","year":"1997","unstructured":"Ghosh MK, Arapostathis A, Marcus SI (1997) Ergodic control of switching diffusions. SIAM J Control Optim 35(6):1952\u20131988","journal-title":"SIAM J Control Optim"},{"issue":"4","key":"195_CR19","doi-asserted-by":"crossref","first-page":"403","DOI":"10.1016\/0021-9991(76)90041-3","volume":"22","author":"DT Gillespie","year":"1976","unstructured":"Gillespie DT (1976) A general method for numerically simulating the stochastic time evolution of coupled chemical reactions. J Comput Phys 22(4):403\u2013434","journal-title":"J Comput Phys"},{"issue":"S7","key":"195_CR20","doi-asserted-by":"crossref","DOI":"10.1186\/1471-2105-11-S7-S10","volume":"11","author":"H Gong","year":"2010","unstructured":"Gong H, Zuliani P, Komuravelli A, Faeder JR, Clarke EM (2010) Analysis and verification of the HMGB1 signaling pathway. BMC Bioinform 11(S7):S10","journal-title":"BMC Bioinform"},{"key":"195_CR21","series-title":"LNCS","first-page":"271","volume-title":"TACAS","author":"R Grosu","year":"2005","unstructured":"Grosu R, Smolka S (2005) Monte Carlo model checking. In: TACAS. LNCS, vol 3440, pp 271\u2013286"},{"key":"195_CR22","first-page":"641","volume-title":"CAV","author":"EM Hahn","year":"2009","unstructured":"Hahn EM, Hermanns H, Wachter B, Zhang L (2009) INFAMY: an infinite-state Markov model checker. In: CAV, pp 641\u2013647"},{"issue":"5","key":"195_CR23","doi-asserted-by":"crossref","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H Hansson","year":"1994","unstructured":"Hansson H, Jonsson B (1994) A logic for reasoning about time and reliability. Form Asp Comput 6(5):512\u2013535","journal-title":"Form Asp Comput"},{"key":"195_CR24","doi-asserted-by":"crossref","first-page":"84","DOI":"10.1109\/QEST.2012.19","volume-title":"QEST 2012: Proceedings of the 9th international conference on quantitative evaluation of systems","author":"D Henriques","year":"2012","unstructured":"Henriques D, Martins J, Zuliani P, Platzer A, Clarke EM (2012) Statistical model checking for Markov decision processes. In: QEST 2012: Proceedings of the 9th international conference on quantitative evaluation of systems. IEEE Press, New York, pp 84\u201393"},{"key":"195_CR25","series-title":"LNCS","first-page":"73","volume-title":"VMCAI","author":"T H\u00e9rault","year":"2004","unstructured":"H\u00e9rault T, Lassaigne R, Magniette F, Peyronnet S (2004) Approximate probabilistic model checking. In: VMCAI. LNCS, vol 2937, pp 73\u201384"},{"issue":"344","key":"195_CR26","doi-asserted-by":"crossref","DOI":"10.1126\/stke.3442006re6","volume":"18","author":"WS Hlavacek","year":"2006","unstructured":"Hlavacek WS, Faeder JR, Blinov ML, Posner RG, Hucka M, Fontana W (2006) Rules for modeling signal-transduction system. Sci STKE 18(344):re6","journal-title":"Sci STKE"},{"issue":"301","key":"195_CR27","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1080\/01621459.1963.10500830","volume":"58","author":"W Hoeffding","year":"1963","unstructured":"Hoeffding W (1963) Probability inequalities for sums of bounded random variables. J Am Stat Assoc 58(301):13\u201330","journal-title":"J Am Stat Assoc"},{"key":"195_CR28","volume-title":"Theory of probability","author":"H Jeffreys","year":"1961","unstructured":"Jeffreys H (1961) Theory of probability. Clarendon, Oxford"},{"key":"195_CR29","series-title":"LNCS","first-page":"218","volume-title":"CMSB","author":"SK Jha","year":"2009","unstructured":"Jha SK, Clarke EM, Langmead CJ, Legay A, Platzer A, Zuliani P (2009) A Bayesian approach to model checking biological systems. In: CMSB. LNCS, vol 5688, pp 218\u2013234"},{"issue":"4","key":"195_CR30","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1007\/BF01995674","volume":"2","author":"R Koymans","year":"1990","unstructured":"Koymans R (1990) Specifying real-time properties with metric temporal logic. Real-Time Syst 2(4):255\u2013299","journal-title":"Real-Time Syst"},{"key":"195_CR31","series-title":"LNCS","first-page":"585","volume-title":"CAV","author":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska M, Norman G, Parker D (2011) PRISM 4.0: verification of probabilistic real-time systems. In: CAV. LNCS, vol 6806, pp 585\u2013591"},{"key":"195_CR32","series-title":"LNCS","first-page":"234","volume-title":"CAV","author":"MZ Kwiatkowska","year":"2006","unstructured":"Kwiatkowska MZ, Norman G, Parker D (2006) Symmetry reduction for probabilistic model checking. In: CAV. LNCS, vol 4144, pp 234\u2013248"},{"key":"195_CR33","first-page":"201","volume-title":"CSB","author":"CJ Langmead","year":"2009","unstructured":"Langmead CJ (2009) Generalized queries and Bayesian statistical model checking in dynamic Bayesian networks: application to personalized medicine. In: CSB, pp 201\u2013212"},{"key":"195_CR34","series-title":"LNCS","first-page":"152","volume-title":"FORMATS","author":"O Maler","year":"2004","unstructured":"Maler O, Nickovic D (2004) Monitoring temporal properties of continuous signals. In: FORMATS. LNCS, vol 3253, pp 152\u2013166"},{"key":"195_CR35","first-page":"460","volume-title":"HSCC","author":"J Meseguer","year":"2006","unstructured":"Meseguer J, Sharykin R (2006) Specification and analysis of distributed object-based stochastic hybrid systems. In: Hespanha JP, Tiwari A (eds) HSCC, vol 3927. Springer, Berlin, pp 460\u2013475"},{"key":"195_CR36","series-title":"LNCS","first-page":"1","volume-title":"Proc of FORMATS","author":"J Ouaknine","year":"2008","unstructured":"Ouaknine J, Worrell J (2008) Some recent results in metric temporal logic. In: Proc of FORMATS. LNCS, vol 5215, pp 1\u201313"},{"key":"195_CR37","series-title":"LNCS","first-page":"431","volume-title":"CADE","author":"A Platzer","year":"2011","unstructured":"Platzer A (2011) Stochastic differential dynamic logic for stochastic hybrid programs. In: Bj\u00f8rner N, Sofronie-Stokkermans V (eds) CADE. LNCS, vol 6803. Springer, Berlin, pp 431\u2013445"},{"key":"195_CR38","first-page":"46","volume-title":"FOCS","author":"A Pnueli","year":"1977","unstructured":"Pnueli A (1977) The temporal logic of programs. In: FOCS. IEEE Press, New York, pp 46\u201357"},{"key":"195_CR39","volume-title":"The Bayesian choice","author":"CP Robert","year":"2001","unstructured":"Robert CP (2001) The Bayesian choice. Springer, Berlin"},{"key":"195_CR40","volume-title":"Simulation and the Monte Carlo method","author":"RY Rubinstein","year":"2008","unstructured":"Rubinstein RY, Kroese DP (2008) Simulation and the Monte Carlo method. Wiley, New York"},{"key":"195_CR41","series-title":"LNCS","first-page":"202","volume-title":"CAV","author":"K Sen","year":"2004","unstructured":"Sen K, Viswanathan M, Agha G (2004) Statistical model checking of black-box probabilistic systems. In: CAV. LNCS, vol 3114, pp 202\u2013215"},{"key":"195_CR42","series-title":"LNCS","first-page":"266","volume-title":"CAV","author":"K Sen","year":"2005","unstructured":"Sen K, Viswanathan M, Agha G (2005) On statistical model checking of stochastic systems. In: CAV. LNCS, vol 3576, pp 266\u2013280"},{"key":"195_CR43","volume-title":"Probability","author":"AN Shiryaev","year":"1995","unstructured":"Shiryaev AN (1995) Probability. Springer, Berlin"},{"key":"195_CR44","unstructured":"Tiwari A (2002) Formal semantics and analysis methods for Simulink Stateflow models. Technical report, SRI International"},{"issue":"1","key":"195_CR45","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1007\/s10703-007-0044-3","volume":"32","author":"A Tiwari","year":"2008","unstructured":"Tiwari A (2008) Abstractions for hybrid systems. Form Methods Syst Des 32(1):57\u201383","journal-title":"Form Methods Syst Des"},{"issue":"2","key":"195_CR46","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1214\/aoms\/1177731118","volume":"16","author":"A Wald","year":"1945","unstructured":"Wald A (1945) Sequential tests of statistical hypotheses. Ann Math Stat 16(2):117\u2013186","journal-title":"Ann Math Stat"},{"key":"195_CR47","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1109\/ASPDAC.2011.5722168","volume-title":"ASP-DAC 2011: Proceedings of the 16th Asia and South Pacific design automation conference","author":"Y-C Wang","year":"2011","unstructured":"Wang Y-C, Komuravelli A, Zuliani P, Clarke EM (2011) Analog circuit verification by statistical model checking. In: ASP-DAC 2011: Proceedings of the 16th Asia and South Pacific design automation conference. IEEE Press, New York, pp 1\u20136"},{"issue":"3","key":"195_CR48","doi-asserted-by":"crossref","first-page":"216","DOI":"10.1007\/s10009-005-0187-8","volume":"8","author":"HLS Younes","year":"2006","unstructured":"Younes HLS, Kwiatkowska MZ, Norman G, Parker D (2006) Numerical vs statistical probabilistic model checking. Int J Softw Tools Technol Transf 8(3):216\u2013228","journal-title":"Int J Softw Tools Technol Transf"},{"key":"195_CR49","first-page":"81","volume-title":"AIPS workshop on planning via model checking","author":"HLS Younes","year":"2002","unstructured":"Younes HLS, Musliner DJ (2002) Probabilistic plan verification through acceptance sampling. In: AIPS workshop on planning via model checking, pp 81\u201388"},{"issue":"9","key":"195_CR50","doi-asserted-by":"crossref","first-page":"1368","DOI":"10.1016\/j.ic.2006.05.002","volume":"204","author":"HLS Younes","year":"2006","unstructured":"Younes HLS, Simmons RG (2006) Statistical probabilistic model checking with a focus on time-bounded properties. Inf Comput 204(9):1368\u20131409","journal-title":"Inf Comput"},{"issue":"3","key":"195_CR51","doi-asserted-by":"crossref","first-page":"339","DOI":"10.1109\/12.2171","volume":"37","author":"PS Yu","year":"1988","unstructured":"Yu PS, Krishna CM, Lee Y-H (1988) Optimal design and sequential analysis of VLSI testing strategy. IEEE Trans Comput 37(3):339\u2013347","journal-title":"IEEE Trans Comput"},{"key":"195_CR52","doi-asserted-by":"crossref","unstructured":"Zuliani P, Platzer A, Clarke EM (2010) Bayesian statistical model checking with application to Stateflow\/Simulink verification. Technical report CMU-CS-10-100, Computer Science Department, Carnegie Mellon University","DOI":"10.1145\/1755952.1755987"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-013-0195-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-013-0195-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-013-0195-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,3,4]],"date-time":"2022-03-04T22:13:06Z","timestamp":1646431986000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-013-0195-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,8,27]]},"references-count":52,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2013,10]]}},"alternative-id":["195"],"URL":"https:\/\/doi.org\/10.1007\/s10703-013-0195-3","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,8,27]]}}}