{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,15]],"date-time":"2026-07-15T15:36:02Z","timestamp":1784129762636,"version":"3.55.0"},"publisher-location":"Berlin, Heidelberg","reference-count":43,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642166112","type":"print"},{"value":"9783642166129","type":"electronic"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"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":[[2010]]},"DOI":"10.1007\/978-3-642-16612-9_11","type":"book-chapter","created":{"date-parts":[[2010,11,17]],"date-time":"2010-11-17T11:45:14Z","timestamp":1289994314000},"page":"122-135","source":"Crossref","is-referenced-by-count":296,"title":["Statistical Model Checking: An Overview"],"prefix":"10.1007","author":[{"given":"Axel","family":"Legay","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Beno\u00eet","family":"Delahaye","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Saddek","family":"Bensalem","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"11_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/11944836_25","volume-title":"FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science","author":"A. Bauer","year":"2006","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: Monitoring of real-time properties. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol.\u00a04337, pp. 260\u2013272. Springer, Heidelberg (2006)"},{"issue":"6","key":"11_CR2","doi-asserted-by":"publisher","first-page":"524","DOI":"10.1109\/TSE.2003.1205180","volume":"29","author":"C. Baier","year":"2003","unstructured":"Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for continuous-time markov chains. IEEE Trans. Software Eng.\u00a029(6), 524\u2013541 (2003)","journal-title":"IEEE Trans. Software Eng."},{"key":"11_CR3","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":"11_CR4","doi-asserted-by":"crossref","unstructured":"Basu, A., Bensalem, S., Bozga, M., Caillaud, B., Delahaye, B., Legay, A.: Statistical abstraction and model-checking of large heterogeneous systems. Technical report, INRIA (2010)","DOI":"10.1007\/978-3-642-13464-7_4"},{"key":"11_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/978-3-540-27813-9_15","volume-title":"Computer Aided Verification","author":"D. Bustan","year":"2004","unstructured":"Bustan, D., Rubin, S., Vardi, M.Y.: Verifying omega-regular properties of markov chains. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 189\u2013201. Springer, Heidelberg (2004)"},{"key":"11_CR6","unstructured":"Carnegie Mellon University. A Bayesian Approach to Model Checking Biological Systems (under submission, 2009)"},{"key":"11_CR7","first-page":"131","volume-title":"QEST","author":"F. Ciesinski","year":"2006","unstructured":"Ciesinski, F., Baier, C.: Liquor: A tool for qualitative and quantitative linear time analysis of reactive systems. In: QEST, pp. 131\u2013132. IEEE, Los Alamitos (2006)"},{"key":"11_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.: On probabilistic computation tree logic. In: Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P., Siegle, M. (eds.) Validation of Stochastic Systems. LNCS, vol.\u00a02925, pp. 147\u2013188. Springer, Heidelberg (2004)"},{"key":"11_CR9","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Donz\u00e9, A., Legay, A.: Statistical model checking of mixed-analog circuits with an application to a third order delta-sigma modulator. In: HVC 2008. LNCS, vol.\u00a05394, pp. 149\u2013163. Springer, Heidelberg (2008)","DOI":"10.1007\/978-3-642-01702-5_16"},{"key":"11_CR10","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Donz\u00e9, A., Legay, A.: On simulation-based probabilistic model checking of mixed-analog circuits. Formal Methods in System Design (2009) (to appear)","DOI":"10.1007\/s10703-009-0076-y"},{"key":"11_CR11","series-title":"Lecture Notes in Bioinformatics","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/978-3-540-88562-7_18","volume-title":"Computational Methods in Systems Biology","author":"E.M. Clarke","year":"2008","unstructured":"Clarke, E.M., Faeder, J.R., Langmead, C.J., Harris, L.A., Jha, S.K., Legay, A.: Statistical model checking in biolab: Applications to the automated analysis of t-cell receptor signaling pathway. In: Heiner, M., Uhrmacher, A.M. (eds.) CMSB 2008. LNCS (LNBI), vol.\u00a05307, pp. 231\u2013250. Springer, Heidelberg (2008)"},{"key":"11_CR12","unstructured":"Cmacs, http:\/\/cmacs.cs.cmu.edu\/"},{"issue":"4","key":"11_CR13","doi-asserted-by":"publisher","first-page":"857","DOI":"10.1145\/210332.210339","volume":"42","author":"C. Courcoubetis","year":"1995","unstructured":"Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. Journal of the ACM\u00a042(4), 857\u2013907 (1995)","journal-title":"Journal of the ACM"},{"key":"11_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-540-30494-4_3","volume-title":"Formal Methods in Computer-Aided Design","author":"T. Dang","year":"2004","unstructured":"Dang, T., Donze, A., Maler, O.: Verification of analog and mixed-signal circuits using hybrid systems techniques. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol.\u00a03312, pp. 21\u201336. Springer, Heidelberg (2004)"},{"key":"11_CR15","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1145\/1066677.1066712","volume-title":"SAC 2005: Proceedings of the 2005 ACM symposium on Applied computing","author":"J.R. Faeder","year":"2005","unstructured":"Faeder, J.R., Blinov, M.L., Hlavacek, W.S.: Graphical rule-based representation of signal-transduction networks. In: SAC 2005: Proceedings of the 2005 ACM symposium on Applied computing, pp. 133\u2013140. ACM, New York (2005)"},{"key":"11_CR16","series-title":"Methods in Molecular Biology","volume-title":"Systems Biology","author":"J.R. Faeder","year":"2008","unstructured":"Faeder, J.R., Blinov, M.L., Hlavacek, W.S.: Rule-based modeling of biochemical systems with BioNetGen. In: Maly, I.V. (ed.) Systems Biology. Methods in Molecular Biology. Humana Press, Totowa (2008)"},{"key":"11_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/978-3-540-31980-1_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Grosu","year":"2005","unstructured":"Grosu, R., Smolka, S.A.: Monte carlo model checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 271\u2013286. Springer, Heidelberg (2005)"},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"Gupta, S., Krogh, B.H., Rutenbar, R.A.: Towards formal verification of analog designs. In: ICCAD, pp. 210\u2013217 (2004)","DOI":"10.1109\/ICCAD.2004.1382573"},{"key":"11_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/3-540-46002-0_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. Havelund","year":"2002","unstructured":"Havelund, K., Rosu, G.: Synthesizing monitors for safety properties. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, pp. 342\u2013356. Springer, Heidelberg (2002)"},{"key":"11_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/978-3-540-24622-0_8","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"T. H\u00e9rault","year":"2004","unstructured":"H\u00e9rault, T., Lassaigne, R., Magniette, F., Peyronnet, S.: Approximate probabilistic model checking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 73\u201384. Springer, Heidelberg (2004)"},{"key":"11_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-540-70545-1_16","volume-title":"Computer Aided Verification","author":"H. Hermanns","year":"2008","unstructured":"Hermanns, H., Wachter, B., Zhang, L.: Probabilistic cegar. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 162\u2013175. Springer, Heidelberg (2008)"},{"key":"11_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1007\/978-3-540-77966-7_9","volume-title":"Hardware and Software: Verification and Testing","author":"D.N. Jansen","year":"2008","unstructured":"Jansen, D.N., Katoen, J., Oldenkamp, M., Stoelinga, M., Zapreev, I.S.: How fast and fat is your probabilistic model checker? an experimental performance comparison. In: Yorav, K. (ed.) HVC 2007. LNCS, vol.\u00a04899, pp. 69\u201385. Springer, Heidelberg (2008)"},{"key":"11_CR23","first-page":"31","volume-title":"Proc. of 6th Int. Conference on the Quantitative Evaluation of Systems (QEST)","author":"J.-P. Katoen","year":"2009","unstructured":"Katoen, J.-P., Zapreev, I.S.: Simulation-based ctmc model checking: An empirical evaluation. In: Proc. of 6th Int. Conference on the Quantitative Evaluation of Systems (QEST), pp. 31\u201340. IEEE Computer Society, Los Alamitos (2009)"},{"key":"11_CR24","first-page":"167","volume-title":"Proc. of 6th Int. Conference on the Quantitative Evaluation of Systems (QEST)","author":"J.-P. Katoen","year":"2009","unstructured":"Katoen, J.-P., Zapreev, I.S., Hahn, E.M., Hermanns, H., Jansen, D.N.: The ins and outs of the probabilistic model checker mrmc. In: Proc. of 6th Int. Conference on the Quantitative Evaluation of Systems (QEST), pp. 167\u2013176. IEEE Computer Society Press, Los Alamitos (2009)"},{"key":"11_CR25","first-page":"322","volume-title":"QEST","author":"M.Z. Kwiatkowska","year":"2004","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: Prism 2.0: A tool for probabilistic model checking. In: QEST, pp. 322\u2013323. IEEE, Los Alamitos (2004)"},{"key":"11_CR26","doi-asserted-by":"crossref","unstructured":"Laplante, S., Lassaigne, R., Magniez, F., Peyronnet, S., de Rougemont, M.: Probabilistic abstraction for model checking: An approach based on property testing. ACM Trans. Comput. Log. 8(4) (2007)","DOI":"10.1145\/1276920.1276922"},{"issue":"1","key":"11_CR27","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(91)90030-6","volume":"94","author":"K.G. Larsen","year":"1991","unstructured":"Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Inf. Comput.\u00a094(1), 1\u201328 (1991)","journal-title":"Inf. Comput."},{"key":"11_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"186","DOI":"10.1007\/978-3-642-10373-5_10","volume-title":"Formal Methods and Software Engineering","author":"M.G. Merayo","year":"2009","unstructured":"Merayo, M.G., Hwang, I., N\u00fa\u00f1ez, M., Cavalli, A.R.: A statistical approach to test stochastic and probabilistic systems. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol.\u00a05885, pp. 186\u2013205. Springer, Heidelberg (2009)"},{"key":"11_CR29","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proc. 18th Annual Symposium on Foundations of Computer Science (FOCS), pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"11_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1007\/978-3-642-04761-9_11","volume-title":"Automated Technology for Verification and Analysis","author":"D.E. Rabih","year":"2009","unstructured":"Rabih, D.E., Pekergin, N.: Statistical model checking using perfect simulation. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol.\u00a05799, pp. 120\u2013134. Springer, Heidelberg (2009)"},{"key":"11_CR31","series-title":"CRM Monograph Series","doi-asserted-by":"publisher","DOI":"10.1090\/crmm\/023","volume-title":"Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems, P. Panangaden and F. van Breugel (eds.)","author":"J. Rutten","year":"2004","unstructured":"Rutten, J., Kwiatkowska, M., Norman, G., Parker, D.: Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems. In: Panangaden, P., van Breugel, F. (eds.) Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems, P. Panangaden and F. van Breugel (eds.). CRM Monograph Series, vol.\u00a023. American Mathematical Society, Providence (2004)"},{"key":"11_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/978-3-540-27813-9_16","volume-title":"Computer Aided Verification","author":"K. Sen","year":"2004","unstructured":"Sen, K., Viswanathan, M., Agha, G.: Statistical model checking of black-box probabilistic systems. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 202\u2013215. Springer, Heidelberg (2004)"},{"key":"11_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/11513988_26","volume-title":"Computer Aided Verification","author":"K. Sen","year":"2005","unstructured":"Sen, K., Viswanathan, M., Agha, G.: On statistical model checking of stochastic systems. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 266\u2013280. Springer, Heidelberg (2005)"},{"key":"11_CR34","first-page":"251","volume-title":"QEST","author":"K. Sen","year":"2005","unstructured":"Sen, K., Viswanathan, M., Agha, G.A.: Vesta: A statistical model-checker and analyzer for probabilistic systems. In: QEST, pp. 251\u2013252. IEEE Computer Society, Los Alamitos (2005)"},{"key":"11_CR35","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state programs. In: FOCS, pp. 327\u2013338 (1985)","DOI":"10.1109\/SFCS.1985.12"},{"issue":"2","key":"11_CR36","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. Annals of Mathematical Statistics\u00a016(2), 117\u2013186 (1945)","journal-title":"Annals of Mathematical Statistics"},{"key":"11_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/11513988_25","volume-title":"Computer Aided Verification","author":"H.L.S. Younes","year":"2005","unstructured":"Younes, H.L.S.: Probabilistic verification for \u201dblack-box\u201d systems. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 253\u2013265. Springer, Heidelberg (2005)"},{"key":"11_CR38","unstructured":"Younes, H.L.S.: Verification and Planning for Stochastic Processes with Asynchronous Events. PhD thesis, Carnegie Mellon (2005)"},{"key":"11_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1007\/11513988_43","volume-title":"Computer Aided Verification","author":"H.L.S. Younes","year":"2005","unstructured":"Younes, H.L.S.: Ymer: A statistical model checker. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 429\u2013433. Springer, Heidelberg (2005)"},{"key":"11_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/11609773_10","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"H.L.S. Younes","year":"2005","unstructured":"Younes, H.L.S.: Error control for probabilistic model checking. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 142\u2013156. Springer, Heidelberg (2005)"},{"issue":"3","key":"11_CR41","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/s10009-005-0187-8","volume":"8","author":"H.L.S. Younes","year":"2006","unstructured":"Younes, H.L.S., Kwiatkowska, M.Z., Norman, G., Parker, D.: Numerical vs. statistical probabilistic model checking. STTT\u00a08(3), 216\u2013228 (2006)","journal-title":"STTT"},{"key":"11_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/3-540-45657-0_17","volume-title":"Computer Aided Verification","author":"H.L.S. Younes","year":"2002","unstructured":"Younes, H.L.S., Simmons, R.G.: Probabilistic verification of discrete event systems using acceptance sampling. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 223\u2013235. Springer, Heidelberg (2002)"},{"issue":"9","key":"11_CR43","doi-asserted-by":"publisher","first-page":"1368","DOI":"10.1016\/j.ic.2006.05.002","volume":"204","author":"H.L.S. Younes","year":"2006","unstructured":"Younes, H.L.S., Simmons, R.G.: Statistical probabilistic model checking with a focus on time-bounded properties. Information and Computation\u00a0204(9), 1368\u20131409 (2006)","journal-title":"Information and Computation"}],"container-title":["Lecture Notes in Computer Science","Runtime Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-16612-9_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,6]],"date-time":"2019-06-06T09:57:24Z","timestamp":1559815044000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-16612-9_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642166112","9783642166129"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-16612-9_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}