{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:13:51Z","timestamp":1742912031752,"version":"3.40.3"},"publisher-location":"Cham","reference-count":44,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319471686"},{"type":"electronic","value":"9783319471693"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-47169-3_62","type":"book-chapter","created":{"date-parts":[[2016,10,4]],"date-time":"2016-10-04T17:56:23Z","timestamp":1475603783000},"page":"843-862","source":"Crossref","is-referenced-by-count":6,"title":["On the Power of Statistical Model Checking"],"prefix":"10.1007","author":[{"given":"Kim G.","family":"Larsen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Axel","family":"Legay","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,10,5]]},"reference":[{"issue":"1","key":"62_CR1","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1006\/inco.1993.1024","volume":"104","author":"R Alur","year":"1993","unstructured":"Alur, R., Courcoubetis, C., Dill, D.L.: Model-checking in dense real-time. Inf. Comput. 104(1), 2\u201334 (1993)","journal-title":"Inf. Comput."},{"issue":"2","key":"62_CR2","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183\u2013235 (1994)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"62_CR3","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1007\/s10009-003-0111-z","volume":"7","author":"G Behrmann","year":"2005","unstructured":"Behrmann, G.: Distributed reachability analysis in timed automata. Int. J. Softw. Tools Technol. Transfer 7(1), 19\u201330 (2005)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"62_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1007\/978-3-540-73368-3_14","volume-title":"Computer Aided Verification","author":"G Behrmann","year":"2007","unstructured":"Behrmann, G., Cougnard, A., David, A., Fleury, E., Larsen, K.G., Lime, D.: UPPAAL-Tiga: time for playing games!. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 121\u2013125. Springer, Heidelberg (2007)"},{"key":"62_CR5","unstructured":"Behrmann, G., David, A., Larsen, K.G., H\u00e5kansson, J., Pettersson, P., Yi, W., Hendriks, M.: Uppaal 4.0. In: QEST. IEEE Computer Society (2006)"},{"issue":"2","key":"62_CR6","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1002\/spe.1006","volume":"41","author":"G Behrmann","year":"2011","unstructured":"Behrmann, G., David, A., Larsen, K.G., Pettersson, P., Yi, W.: Developing uppaal over 15 years. Softw. Pract. Exper. 41(2), 133\u2013142 (2011)","journal-title":"Softw. Pract. Exper."},{"key":"62_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/3-540-44829-2_15","volume-title":"Model Checking Software","author":"G Behrmann","year":"2003","unstructured":"Behrmann, G., David, A., Larsen, K.G., Yi, W.: Unification & sharing in timed automata verification. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 225\u2013229. Springer, Heidelberg (2003). doi: 10.1007\/3-540-44829-2_15"},{"key":"62_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/3-540-45319-9_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Behrmann","year":"2001","unstructured":"Behrmann, G., Fehnker, A., Hune, T., Larsen, K., Pettersson, P., Romijn, J.: Efficient guiding towards cost-optimality in UPPAAL. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 174\u2013188. Springer, Heidelberg (2001). doi: 10.1007\/3-540-45319-9_13"},{"key":"62_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/3-540-45351-2_15","volume-title":"Hybrid Systems: Computation and Control","author":"G Behrmann","year":"2001","unstructured":"Behrmann, G., Fehnker, A., Hune, T., Larsen, K., Pettersson, P., Romijn, J., Vaandrager, F.: Minimum-cost reachability for priced time automata. In: Benedetto, M.D., Sangiovanni-Vincentelli, A. (eds.) HSCC 2001. LNCS, vol. 2034, pp. 147\u2013161. Springer, Heidelberg (2001). doi: 10.1007\/3-540-45351-2_15"},{"key":"62_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/10722167_19","volume-title":"Computer Aided Verification","author":"G Behrmann","year":"2000","unstructured":"Behrmann, G., Hune, T., Vaandrager, F.: Distributing timed model checking \u2014 how the search order matters. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 216\u2013231. Springer, Heidelberg (2000). doi: 10.1007\/10722167_19"},{"key":"62_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/3-540-48683-6_30","volume-title":"Computer Aided Verification","author":"G Behrmann","year":"1999","unstructured":"Behrmann, G., Larsen, K.G., Pearson, J., Weise, C., Yi, W.: Efficient timed reachability analysis using clock difference diagrams. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol. 1633, pp. 341\u2013353. Springer, Heidelberg (1999). doi: 10.1007\/3-540-48683-6_30"},{"key":"62_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-642-40196-1_12","volume-title":"Quantitative Evaluation of Systems","author":"B Boyer","year":"2013","unstructured":"Boyer, B., Corre, K., Legay, A., Sedwards, S.: PLASMA-lab: A Flexible, Distributable Statistical Model Checking Library. In: Joshi, K., Siegle, M., Stoelinga, M., D\u2019Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 160\u2013164. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-40196-1_12"},{"key":"62_CR13","doi-asserted-by":"crossref","unstructured":"Bulychev, P.E., David, A., Larsen, K.G., Legay, A., Mikucionis, M.: Computing nash equilibrium in wireless ad hoc networks: a simulation-based approach. In: IWIGP. EPTCS, vol. 78 (2012)","DOI":"10.4204\/EPTCS.78.1"},{"key":"62_CR14","doi-asserted-by":"crossref","unstructured":"Colombo, A., Fontanelli, D., Gandhi, D., De Angeli, A., Palopoli, L., Sedwards, S., Legay, A.: Behavioural templates improve robot motion planning with social force model in human environments. In: EFTA. IEEE (2013)","DOI":"10.1109\/ETFA.2013.6648081"},{"key":"62_CR15","doi-asserted-by":"crossref","unstructured":"Colombo, A., Fontanelli, D., Legay, A., Palopoli, L., Sedwards, S.: Motion planning in crowds using statistical model checking to enhance the social force model. In: CDC. IEEE (2013)","DOI":"10.1109\/CDC.2013.6760437"},{"key":"62_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/978-3-319-11936-6_10","volume-title":"Automated Technology for Verification and Analysis","author":"A David","year":"2014","unstructured":"David, A., Jensen, P.G., Larsen, K.G., Legay, A., Lime, D., S\u00f8rensen, M.G., Taankvist, J.H.: On time with minimal expected cost!. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 129\u2013145. Springer, Heidelberg (2014). doi: 10.1007\/978-3-319-11936-6_10"},{"key":"62_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1007\/978-3-662-46681-0_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A David","year":"2015","unstructured":"David, A., Jensen, P.G., Larsen, K.G., Miku\u010dionis, M., Taankvist, J.H.: Uppaal Stratego. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 206\u2013211. Springer, Heidelberg (2015). doi: 10.1007\/978-3-662-46681-0_16"},{"issue":"2","key":"62_CR18","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1007\/s10009-014-0331-4","volume":"17","author":"A David","year":"2015","unstructured":"David, A., Larsen, K.G., Legay, A., Mikucionis, M.: Schedulability of herschel revisited using statistical model checking. Int. J. Softw. Tools Technol. Transfer 17(2), 187\u2013199 (2015)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"62_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1007\/978-3-642-34026-0_29","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation","author":"A David","year":"2012","unstructured":"David, A., Larsen, K.G., Legay, A., Miku\u010dionis, M., Poulsen, D.B., Sedwards, S.: Runtime verification of biological systems. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part I. LNCS, vol. 7609, pp. 388\u2013404. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-34026-0_29"},{"issue":"3","key":"62_CR20","doi-asserted-by":"crossref","first-page":"351","DOI":"10.1007\/s10009-014-0323-4","volume":"17","author":"A David","year":"2015","unstructured":"David, A., Larsen, K.G., Legay, A., Mikucionis, M., Poulsen, D.B., Sedwards, S.: Statistical model checking for biological systems. Int. J. Softw. Tools Technol. Transfer 17(3), 351\u2013367 (2015)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"62_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/978-3-642-22110-1_27","volume-title":"Computer Aided Verification","author":"A David","year":"2011","unstructured":"David, A., Larsen, K.G., Legay, A., Miku\u010dionis, M., Wang, Z.: Time for statistical model checking of real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 349\u2013355. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-22110-1_27"},{"key":"62_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1007\/3-540-45923-5_15","volume-title":"Fundamental Approaches to Software Engineering","author":"A David","year":"2002","unstructured":"David, A., M\u00f6ller, M.O., Yi, W.: Formal verification of UML statecharts with real-time extensions. In: Kutsche, R.-D., Weber, H. (eds.) FASE 2002. LNCS, vol. 2306, pp. 218\u2013232. Springer, Heidelberg (2002). doi: 10.1007\/3-540-45923-5_15"},{"issue":"5","key":"62_CR23","doi-asserted-by":"crossref","first-page":"4282","DOI":"10.1103\/PhysRevE.51.4282","volume":"51","author":"D Helbing","year":"1995","unstructured":"Helbing, D., Moln\u00e1r, P.: Social force model for pedestrian dynamics. Phys. Rev. E 51(5), 4282\u20134286 (1995)","journal-title":"Phys. Rev. E"},{"key":"62_CR24","doi-asserted-by":"crossref","unstructured":"Hendriks, M., Larsen, K.G.: Exact acceleration of real-time model checking. In: Electronic Notes in Theoretical Computer Science, vol. 65. Elsevier Science Publishers, April 2002","DOI":"10.1016\/S1571-0661(04)80473-0"},{"key":"62_CR25","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Ho, P.: Algorithmic analysis of nonlinear hybrid systems. In: CAV","DOI":"10.1007\/3-540-60045-0_53"},{"key":"62_CR26","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. 2937, pp. 73\u201384. Springer, Heidelberg (2004). doi: 10.1007\/978-3-540-24622-0_8"},{"key":"62_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"498","DOI":"10.1007\/978-3-642-28756-5_37","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C Jegourel","year":"2012","unstructured":"Jegourel, C., Legay, A., Sedwards, S.: A platform for high performance statistical model checking \u2013 PLASMA. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 498\u2013503. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-28756-5_37"},{"key":"62_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/978-3-642-31424-7_26","volume-title":"Computer Aided Verification","author":"C Jegourel","year":"2012","unstructured":"Jegourel, C., Legay, A., Sedwards, S.: Cross-entropy optimisation of importance sampling parameters for statistical model checking. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 327\u2013342. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-31424-7_26"},{"key":"62_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1007\/978-3-642-39799-8_38","volume-title":"Computer Aided Verification","author":"C Jegourel","year":"2013","unstructured":"Jegourel, C., Legay, A., Sedwards, S.: Importance splitting for statistical model checking rare properties. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 576\u2013591. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-39799-8_38"},{"key":"62_CR30","unstructured":"J\u00e9gourel, C., Legay, A., Sedwards, S., Traonouez, L.: Distributed verification of rare properties using importance splitting observers. ECEASST (2015)"},{"issue":"5","key":"62_CR31","first-page":"263","volume":"1","author":"H Kahn","year":"1953","unstructured":"Kahn, H., Marshall, A.W.: Methods of reducing sample size in Monte Carlo computations. Oper. Res. 1(5), 263\u2013278 (1953)","journal-title":"Oper. Res."},{"key":"62_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"493","DOI":"10.1007\/3-540-44585-4_47","volume-title":"Computer Aided Verification","author":"K Larsen","year":"2001","unstructured":"Larsen, K., Behrmann, G., Brinksma, E., Fehnker, A., Hune, T., Pettersson, P., Romijn, J.: As cheap as possible: effcient cost-optimal reachability for priced timed automata. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 493\u2013505. Springer, Heidelberg (2001). doi: 10.1007\/3-540-44585-4_47"},{"issue":"1","key":"62_CR33","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"KG Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a nutshell. Int. J. Softw. Tools Technol. Transfer 1(1), 134\u2013152 (1997)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"issue":"1","key":"62_CR34","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0890-5401(91)90030-6","volume":"94","author":"KG Larsen","year":"1991","unstructured":"Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Inf. Comput. 94(1), 1\u201328 (1991)","journal-title":"Inf. Comput."},{"key":"62_CR35","doi-asserted-by":"crossref","unstructured":"Larsson, F., Larsen, K.G., Pettersson, P., Yi, W.: Efficient verification of real-time systems: compact data structures and state-space reduction. In: Proceedings of the 18th IEEE Real-Time Systems Symposium. IEEE Computer Society Press, December 1997","DOI":"10.1109\/REAL.1997.641265"},{"issue":"1","key":"62_CR36","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(1), 29\u201335 (1959)","journal-title":"Ann. Inst. Stat. Math."},{"key":"62_CR37","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. 3114, pp. 202\u2013215. Springer, Heidelberg (2004). doi: 10.1007\/978-3-540-27813-9_16"},{"key":"62_CR38","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. 3576, pp. 266\u2013280. Springer, Heidelberg (2005). doi: 10.1007\/11513988_26"},{"key":"62_CR39","doi-asserted-by":"crossref","unstructured":"Sen, K., Viswanathan, M., Agha, G.A.: VESTA: a statistical model-checker and analyzer for probabilistic systems. In: QEST. IEEE Computer Society (2005)","DOI":"10.1109\/QEST.2005.42"},{"issue":"2","key":"62_CR40","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":"62_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1007\/978-3-319-22975-1_20","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"ER Wognsen","year":"2015","unstructured":"Wognsen, E.R., Haverkort, B.R., Jongerden, M., Hansen, R.R., Larsen, K.G.: A score function for optimizing the cycle-life of battery-powered embedded systems. In: Sankaranarayanan, S., Vicario, E. (eds.) FORMATS 2015. LNCS, vol. 9268, pp. 305\u2013320. Springer, Heidelberg (2015). doi: 10.1007\/978-3-319-22975-1_20"},{"key":"62_CR42","doi-asserted-by":"crossref","unstructured":"Yi, W., Pettersson, P., Daniels, M.: Automatic verification of real-time communicating systems by constraint-solving. In: Proceedings of the 7th IFIP WG6.1 International Conference on Formal Description Techniques VII. Chapman & Hall Ltd., London (1995)","DOI":"10.1007\/978-0-387-34878-0_18"},{"key":"62_CR43","unstructured":"Younes, H.L.S.: Verification and Planning for Stochastic Processes with Asynchronous Events. Ph.D. thesis, Carnegie Mellon (2005)"},{"issue":"2","key":"62_CR44","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/s10703-013-0195-3","volume":"43","author":"P Zuliani","year":"2013","unstructured":"Zuliani, P., Platzer, A., Clarke, E.M.: Bayesian statistical model checking with application to Stateflow\/Simulink verification. Formal Methods Syst. Des. 43(2), 191\u2013232 (2013)","journal-title":"Formal Methods Syst. Des."}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-47169-3_62","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T20:22:07Z","timestamp":1498335727000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-47169-3_62"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319471686","9783319471693"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-47169-3_62","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}