{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,12]],"date-time":"2026-03-12T14:53:14Z","timestamp":1773327194197,"version":"3.50.1"},"reference-count":49,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2015,5,27]],"date-time":"2015-05-27T00:00:00Z","timestamp":1432684800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2015,8]]},"DOI":"10.1007\/s10009-015-0384-z","type":"journal-article","created":{"date-parts":[[2015,5,26]],"date-time":"2015-05-26T07:44:04Z","timestamp":1432626244000},"page":"369-376","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":25,"title":["Statistical model checking: challenges and perspectives"],"prefix":"10.1007","volume":"17","author":[{"given":"Axel","family":"Legay","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mahesh","family":"Viswanathan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,5,27]]},"reference":[{"key":"384_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R.: Timed automata. In: Proc. 11th Int. Conference on Computer Aided Verification (CAV), Lecture Notes in Computer Science, vol. 1633, pp. 8\u201322. Springer, Berlin (1999)","DOI":"10.1007\/3-540-48683-6_3"},{"issue":"6","key":"384_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.R., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for continuous-time Markov chains. IEEE Trans. Softw. Eng. 29(6), 524\u2013541 (2003)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"384_CR3","volume-title":"Principles of Model Checking (Representation and Mind Series)","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking (Representation and Mind Series). The MIT Press, Cambridge (2008)"},{"key":"384_CR4","doi-asserted-by":"crossref","unstructured":"Ball, T., Millstein, T.D., Rajamani, S.K.: Polymorphic predicate abstraction. ACM Trans. Program. Lang. Syst., 27(2), 314\u2013343 (2005)","DOI":"10.1145\/1057387.1057391"},{"key":"384_CR5","doi-asserted-by":"crossref","unstructured":"Ballarini, P.: Analyzing oscillatory trends of discrete-state stochastic processes through HASL statistical model checking. Int. J. Softw. Tools. Technol. Transf. (2015). doi: 10.1007\/s10009-015-0370-5","DOI":"10.1007\/s10009-015-0370-5"},{"issue":"1","key":"384_CR6","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/s10009-011-0201-2","volume":"14","author":"A Basu","year":"2012","unstructured":"Basu, A., Bensalem, S., Bozga, M., Delahaye, B., Legay, A.: Statistical abstraction and model-checking of large heterogeneous systems. Int. J. Softw. Tools Technol. Transf. 14(1), 53\u201372 (2012)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"384_CR7","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without bdds. In: TACAS, LNCS, vol. 1579, pp. 193\u2013207. Springer, Berlin (1999)","DOI":"10.1007\/3-540-49059-0_14"},{"key":"384_CR8","doi-asserted-by":"crossref","unstructured":"Biondi, F., Legay, A., Malacaria, P., Wasowski, A.: Quantifying information leakage of randomized protocols. In: Proceedings of 14th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI\u201913), Rome, Italy, Lecture Notes in Computer Science, vol. 7737, pp. 68\u201387. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-35873-9_7"},{"key":"384_CR9","doi-asserted-by":"crossref","unstructured":"Boyer, B., Corre, K., Legay, A., Sedwards, S.: Plasma-lab: a flexible, distributable statistical model checking library. In: QEST, LNCS, vol. 8054, pp. 160\u2013164 (2013)","DOI":"10.1007\/978-3-642-40196-1_12"},{"key":"384_CR10","doi-asserted-by":"crossref","unstructured":"Broy, M., Jonsson, B., Katoen, J.-P., Leucker, M., Pretschner, A. (eds.) Model-based testing of reactive systems. In: Advanced Lectures the Volume is the Outcome of a Research Seminar that was held in Schloss Dagstuhl in January 2004. Lecture Notes in Computer Science, vol. 3472. Springer, Berlin (2005)","DOI":"10.1007\/b137241"},{"issue":"3","key":"384_CR11","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"R Bryant","year":"1992","unstructured":"Bryant, R.: Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Comput. Surv. 24(3), 293\u2013318 (1992)","journal-title":"ACM Comput. Surv."},{"issue":"2","key":"384_CR12","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"JR Burch","year":"1992","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: $$10^{20}$$ 10 20 states and beyond. Inf. Comput. 98(2), 142\u2013170 (1992)","journal-title":"Inf. Comput."},{"key":"384_CR13","doi-asserted-by":"crossref","unstructured":"Chakraborty, S., Katoen, J.-P., Sher, F., Strelec, M.: Modelling and statistical model checking of a microgrid. Int. J. Softw. Tools. Technol. Transf. (2015). doi: 10.1007\/s10009-014-0345-y","DOI":"10.1007\/s10009-014-0345-y"},{"key":"384_CR14","doi-asserted-by":"crossref","unstructured":"Ciesinski, F., Baier, C.: Liquor: A tool for qualitative and quantitative linear time analysis of reactive systems. In: Proc. of 3rd Int. Conference on the Quantitative Evaluation of Systems (QEST), pp. 131\u2013132. IEEE (2006)","DOI":"10.1109\/QEST.2006.25"},{"key":"384_CR15","doi-asserted-by":"crossref","unstructured":"Ciesinski, F., Gr\u00f6\u00dfer, M.: On probabilistic computation tree logic. In: Validation of Stochastic Systems, LNCS, vol. 2925, pp. 147\u2013188. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-24611-4_5"},{"key":"384_CR16","volume-title":"Model Checking","author":"E Clarke","year":"1999","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"384_CR17","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Logic of Programs, Lecture Notes in Computer Science, vol. 131, pp. 52\u201371. Springer, Berlin (1981)","DOI":"10.1007\/BFb0025774"},{"key":"384_CR18","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Veith, H.: Counterexamples revisited: principles, algorithms, applications. In: Verification: Theory and Practice, Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday, LNCS, vol. 2772, pp. 208\u2013224. Springer, Berlin (2003)","DOI":"10.1007\/978-3-540-39910-0_9"},{"key":"384_CR19","doi-asserted-by":"crossref","first-page":"416","DOI":"10.1016\/j.scico.2013.09.019","volume":"80","author":"A Classen","year":"2014","unstructured":"Classen, A., Cordy, M., Heymans, P., Legay, A., Schobbens, P.: Formal semantics, modular specification, and symbolic verification of product-line behaviour. Sci. Comput. Program. 80, 416\u2013439 (2014)","journal-title":"Sci. Comput. Program."},{"issue":"8","key":"384_CR20","doi-asserted-by":"crossref","first-page":"1069","DOI":"10.1109\/TSE.2012.86","volume":"39","author":"A Classen","year":"2013","unstructured":"Classen, A., Cordy, M., Schobbens, P., Heymans, P., Legay, A., Raskin, J.: Featured transition systems: foundations for verifying variability-intensive systems and their application to LTL model checking. IEEE Trans. Softw. Eng. 39(8), 1069\u20131089 (2013)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"384_CR21","doi-asserted-by":"crossref","unstructured":"Cordy, M., Heymans, P., Legay, A., Schobbens, P., Dawagne, B., Leucker, M.: Counterexample guided abstraction refinement of product-line behavioural models. In: Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE-22), Hong Kong, China, pp. 190\u2013201. ACM (2014)","DOI":"10.1145\/2635868.2635919"},{"issue":"4","key":"384_CR22","doi-asserted-by":"crossref","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. J. ACM 42(4), 857\u2013907 (1995)","journal-title":"J. ACM"},{"key":"384_CR23","doi-asserted-by":"crossref","unstructured":"D\u2019Argenio, P., Legay, A., Sedwards, S., Traonouez, L.-M.: Smart sampling for lightweight verification of Markov decision processes. Int. J. Softw. Tools. Technol. Transf. (2015). doi: 10.1007\/s10009-015-0383-0","DOI":"10.1007\/s10009-015-0383-0"},{"key":"384_CR24","doi-asserted-by":"crossref","unstructured":"David, A., Larsen, K.G., Legay, A., Miku\u010dionis, M., Poulsen, D.B.: UPPAAL SMC tutorial. Int. J. Softw. Tools. Technol. Transf. (2015). doi: 10.1007\/s10009-014-0361-y","DOI":"10.1007\/s10009-014-0361-y"},{"key":"384_CR25","doi-asserted-by":"crossref","unstructured":"David, A., Larsen, K., Legay, A., Wang, Z., Mikucionis, M.: Time for real statistical model-checking: statistical model-checking for real-time systems. In: CAV, LNCS. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-22110-1_27"},{"key":"384_CR26","doi-asserted-by":"crossref","unstructured":"de Alfaro, L.L.D. da Silva, L., Faella, M., Legay, A., Roy, P., Sorea, M.: Sociable interfaces. In: Proc 5th Int. Conference on Frontiers of Combining Systems (FROCOS), Lecture Notes in Computer Science, vol. 3717, pp. 81\u2013105. Springer, Berlin (2005)","DOI":"10.1007\/11559306_5"},{"issue":"1\u20133","key":"384_CR27","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1016\/S0304-3975(03)00361-X","volume":"311","author":"A Dovier","year":"2004","unstructured":"Dovier, A., Piazza, C., Policriti, A.: An efficient algorithm for computing bisimulation equivalence. J. Theor. Comput. Sci. 311(1\u20133), 221\u2013256 (2004)","journal-title":"J. Theor. Comput. Sci."},{"issue":"1\u20132","key":"384_CR28","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1016\/j.tcs.2007.02.055","volume":"380","author":"M Droste","year":"2007","unstructured":"Droste, M., Gastin, P.: Weighted automata and weighted logics. Theor. Comput. Sci. 380(1\u20132), 69\u201386 (2007)","journal-title":"Theor. Comput. Sci."},{"key":"384_CR29","doi-asserted-by":"crossref","unstructured":"Ellen, C., Gerwinn, S., Fr\u00e4nzle, M.: Statistical model checking for stochastic hybrid systems involving nondeterminism over continuous domains. Int. J. Softw. Tools. Technol. Transf. (2014). doi: 10.1007\/s10009-014-0329-y","DOI":"10.1007\/s10009-014-0329-y"},{"key":"384_CR30","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: Proc. 32th Int. Symposium on Principles of Programming Languages (POPL), pp. 110\u2013121. ACM (2005)","DOI":"10.1145\/1040305.1040315"},{"key":"384_CR31","doi-asserted-by":"crossref","unstructured":"Cabodi, G., Camurati, P., Quer, S.: Can bdds compete with sat solvers on bounded model checking? In: Proc. of 39th Design Automation Conference (DAC), pp. 117\u2013122. ACM (2002)","DOI":"10.1145\/513918.513949"},{"key":"384_CR32","doi-asserted-by":"crossref","unstructured":"Hartmanns, A., Timmer, M.: Sound statistical model checking for MDP using partial order and confluence reduction. Int. J. Softw. Tools. Technol. Transf. (2014). doi: 10.1007\/s10009-014-0349-7","DOI":"10.1007\/s10009-014-0349-7"},{"key":"384_CR33","doi-asserted-by":"crossref","unstructured":"Havelund, K., Rou, G.: Synthesizing monitors for safety properties. In: TACAS, LNCS, vol. 2280, pp. 342\u2013356 (2002)","DOI":"10.1007\/3-540-46002-0_24"},{"key":"384_CR34","doi-asserted-by":"crossref","unstructured":"Jha, S.K., Clarke, E.M., Langmead, C.J., Legay, A., Platzer, A., Zuliani, P.: A Bayesian approach to model checking biological systems. In: CMSB, pp. 218\u2013234 (2009)","DOI":"10.1007\/978-3-642-03845-7_15"},{"key":"384_CR35","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: CAV\u201911, LNCS, vol. 6806, pp. 585\u2013591. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"384_CR36","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M. Z., Norman, G., Parker, D.: Prism 2.0: A tool for probabilistic model checking. In: QEST, pp. 322\u2013323. IEEE (2004)","DOI":"10.1109\/QEST.2004.1348048"},{"key":"384_CR37","doi-asserted-by":"crossref","unstructured":"Lassaigne, R., Peyronnet, S.: Approximate planning and verification for large Markov decision processes. Int. J. Softw. Tools. Technol. Transf. (2014). doi: 10.1007\/s10009-014-0344-z","DOI":"10.1007\/s10009-014-0344-z"},{"key":"384_CR38","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1007\/BF02883985","volume":"10","author":"M Okamoto","year":"1959","unstructured":"Okamoto, M.: Some inequalities relating to the partial sum of binomial probabilities. Ann. Inst. Stat. Math. 10, 29\u201335 (1959)","journal-title":"Ann. Inst. Stat. Math."},{"key":"384_CR39","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":"384_CR40","doi-asserted-by":"crossref","unstructured":"Reijsbergen, D., de Boer, P.-T., Scheinhardt, W., Haverkort, B.: On hypothesis testing for statistical model checking. Int. J. Softw. Tools. Technol. Transf. (2014). doi: 10.1007\/s10009-014-0350-1","DOI":"10.1007\/s10009-014-0350-1"},{"key":"384_CR41","doi-asserted-by":"crossref","unstructured":"Roohi, N., Viswanathan, M.: Statistical model checking for unbounded until formulas. Int. J. Softw. Tools. Technol. Transf. (2015). doi: 10.1007\/s10009-015-0368-z","DOI":"10.1007\/s10009-015-0368-z"},{"key":"384_CR42","doi-asserted-by":"crossref","unstructured":"Sen, K., Viswanathan, M., Agha, G.: Statistical model checking of black-box probabilistic systems. In: CAV, LNCS, vol. 3114, pp. 202\u2013215. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-27813-9_16"},{"issue":"2","key":"384_CR43","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1214\/aoms\/1177731118","volume":"16","author":"A Wald","year":"1945","unstructured":"Wald, A.: Sequential tests of statistical hypotheses. Ann. Math. Stat. 16(2), 117\u2013186 (1945)","journal-title":"Ann. Math. Stat."},{"key":"384_CR44","doi-asserted-by":"crossref","unstructured":"Wolper, P., Godefroid, P.: Partial-order methods for temporal verification. In: Proc. 4th Int. Conference on Concurrency Theory (CONCUR), Lecture Notes in Computer Science, vol. 715, pp. 233\u2013246. Springer, Berlin (1993)","DOI":"10.1007\/3-540-57208-2_17"},{"key":"384_CR45","unstructured":"Younes, H.L.S.: Verification and planning for stochastic processes with asynchronous events. PhD thesis, Carnegie Mellon (2005)"},{"key":"384_CR46","doi-asserted-by":"crossref","unstructured":"Younes, H.L.S.: Error control for probabilistic model checking. In: Proc. of 7th Int. Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), LNCS, vol. 3855, pp. 142\u2013156. Springer, Berlin (2006)","DOI":"10.1007\/11609773_10"},{"key":"384_CR47","doi-asserted-by":"crossref","unstructured":"Younes, H.L.S., Simmons, R.G.: Probabilistic verification of discrete event systems using acceptance sampling. In: CAV, LNCS, vol. 2404, pp. 223\u2013235. Springer, Berlin (2002)","DOI":"10.1007\/3-540-45657-0_17"},{"key":"384_CR48","doi-asserted-by":"crossref","unstructured":"Zuliani, P.: Statistical model checking for biological applications (2014). Int. J. Softw. Tools. Technol. Transf. doi: 10.1007\/s10009-014-0343-0","DOI":"10.1007\/s10009-014-0343-0"},{"key":"384_CR49","doi-asserted-by":"crossref","unstructured":"Zuliani, P., Platzer, A., Clarke, E.M.: Bayesian statistical model checking with application to simulink\/stateflow verification. In: HSCC, pp. 243\u2013252. ACM (2010)","DOI":"10.21236\/ADA531406"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-015-0384-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-015-0384-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-015-0384-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,28]],"date-time":"2025-05-28T03:03:48Z","timestamp":1748401428000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-015-0384-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,5,27]]},"references-count":49,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2015,8]]}},"alternative-id":["384"],"URL":"https:\/\/doi.org\/10.1007\/s10009-015-0384-z","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,5,27]]}}}