Advertisement

Statistical Model Checking the 2018 Edition!

  • Kim Guldstrand LarsenEmail author
  • Axel Legay
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11245)

Abstract

This short note introduces statistical model checking and gives a brief overview of the Statistical Model Checking, past present and future session at Isola 2018. This is the fourth edition of the track at Isola.

References

  1. Ashok, P., Brazdil, T., Kretinsky, J., Slamecka, O.: Monte Carlo tree search for verifying reachability in Markov decision processes. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11245, pp. 322–335. Springer, Cham (2018)CrossRefGoogle Scholar
  2. Arora, S., Traonouez, L.-M., Legay, A., Richmond, T.: Statistical model-checking of incomplete stochastic systems. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11245, pp. 354–371. Springer, Cham (2018)CrossRefGoogle Scholar
  3. Basu, A., Bensalem, S., Bozga, M., Delahaye, B., Legay, A.: Statistical abstraction and model-checking of large heterogeneous systems. STTT 14(1), 53–72 (2012)CrossRefGoogle Scholar
  4. ter Beek, M., Basile, D., Ciancia, V.: Statistical model checking a moving block railway signalling scenario with Uppaal SMC. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11245, pp. 372–391. Springer, Cham (2018)Google Scholar
  5. Mediouni, B.L., Nouri, A., Bozga, M., Legay, A., Bensalem, S.: Mitigating security risks through attack strategies exploration. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11245, pp. 392–413. Springer, Cham (2018)CrossRefGoogle Scholar
  6. 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’Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 160–164. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-40196-1_12CrossRefGoogle Scholar
  7. Bianco, A., de Alfaro, L.: Model checking of probabilistic and nondeterministic systems. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol. 1026, pp. 499–513. Springer, Heidelberg (1995).  https://doi.org/10.1007/3-540-60692-0_70CrossRefzbMATHGoogle Scholar
  8. Ballarini, P., Djafri, H., Duflot, M., Haddad, S., Pekergin, N.: COSMOS: a statistical model checker for the hybrid automata stochastic logic. In: QEST, pp. 143–144. IEEE Computer Society (2011)Google Scholar
  9. Bellman, R.: Dynamic Programming. Princeton University Press, Princeton (1957)zbMATHGoogle Scholar
  10. Bogdoll, J., Ferrer Fioriti, L.M., Hartmanns, A., Hermanns, H.: Partial order methods for statistical model checking and simulation. In: Bruni, R., Dingel, J. (eds.) FMOODS/FORTE -2011. LNCS, vol. 6722, pp. 59–74. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-21461-5_4CrossRefGoogle Scholar
  11. Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for continuous-time Markov chains. IEEE 29(6), 524–541 (2003)zbMATHGoogle Scholar
  12. Barbot, B., Haddad, S., Picaronny, C.: Coupling and importance sampling for statistical model checking. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 331–346. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-28756-5_23CrossRefzbMATHGoogle Scholar
  13. Peled, D., Bu, L., Shen, D., Tzirulnikov, Y.: Chasing errors using biasing automata. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11245, pp. 271–286. Springer, Cham (2018)Google Scholar
  14. Clarke, E.M., Emerson, E.A., Sifakis, J.: Model checking: algorithmic verification and debugging. Commun. ACM 52(11), 74–84 (2009)CrossRefGoogle Scholar
  15. Ciesinski, F., Größer, 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. 2925, pp. 147–188. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-24611-4_5CrossRefGoogle Scholar
  16. Cérou, F., Guyader, A.: Adaptive multilevel splitting for rare event analysis. Stoch. Anal. Appl. 25, 417–443 (2007)MathSciNetCrossRefGoogle Scholar
  17. 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–12. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-24372-1_1CrossRefzbMATHGoogle Scholar
  18. De Boer, P.-T., Nicola, V.F., Rubinstein, R.Y.: Adaptive importance sampling simulation of queueing networks. In: Winter Simulation Conference, vol. 1, pp. 646–655 (2000)Google Scholar
  19. David, A., Du, D., Guldstrand Larsen, K., Legay, A., Mikučionis, M.: Optimizing control strategy using statistical model checking. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 352–367. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-38088-4_24CrossRefGoogle Scholar
  20. D’Argenio, P., Hartmanns, A., Sedwards, S.: Lightweight statistical model checking in nondeterministic continuous time. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11245, pp. 336–353. Springer, Cham (2018)CrossRefGoogle Scholar
  21. David, A., Jensen, P.G., Larsen, K.G., Legay, A., Lime, D., Sorensen, M.G., Taankvist, J.HGoogle Scholar
  22. Jegourel, C., Sun, J., Dong, J.-S.: On the sequential Massart algorithm for statistical model checking. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11245, pp. 287–304. Springer, Cham (2018)CrossRefGoogle Scholar
  23. David, A., Larsen, K.G., Legay, A., Mikučionis, 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–355. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-22110-1_27CrossRefGoogle Scholar
  24. Puch, S., Fraenzle, M., Gerwinn, S.: Quantitative risk assessment of safety-critical systems via guided simulation for rare events. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11245, pp. 305–321. Springer, Cham (2018)CrossRefGoogle Scholar
  25. Hermanns, H., Hartmanns, A.: An internet inspired approach to power grid stability. IT Inf. Technol. 55(2), 45–51 (2013)Google Scholar
  26. Hérault, T., Lassaigne, R., Magniette, F., Peyronnet, S.: Approximate probabilistic model checking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 73–84. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-24622-0_8CrossRefzbMATHGoogle Scholar
  27. Henriques, D., Martins, J.G., Zuliani, P., Platzer, A., Clarke, E.M.: Statistical model checking for Markov decision processes. In: 2012 Ninth International Conference on Quantitative Evaluation of Systems, pp. 84–93. IEEE (2012)Google Scholar
  28. Hartmanns, A., Timmer, M.: On-the-fly confluence detection for statistical model checking. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 337–351. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-38088-4_23CrossRefGoogle Scholar
  29. 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–342. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-31424-7_26CrossRefGoogle Scholar
  30. 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–591. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-39799-8_38CrossRefGoogle Scholar
  31. Kahn, H., Marshall, A.W.: Methods of reducing sample size in Monte Carlo computations. Oper. Res. 1(5), 263–278 (1953)Google Scholar
  32. Lassaigne, R., Peyronnet, S.: Approximate planning and verification for large Markov decision processes. In: Proceedings of the 27th Annual ACM Symposium on Applied Computing, pp. 1314–1319. ACM (2012)Google Scholar
  33. Guldstrand Larsen, K., Skou, A., Kim Guldstrand Larsen and Arne Skou: Bisimulation through probabilistic testing. Inf. Comput. 94(1), 1–28 (1991)MathSciNetCrossRefGoogle Scholar
  34. Legay, A., Sedwards, S.: Lightweight Monte Carlo verification of Markov decision processes (2014, submitted)Google Scholar
  35. Okamoto, M.: Some inequalities relating to the partial sum of binomial probabilities. Ann. Inst. Stat. Math. 10, 29–35 (1959)MathSciNetCrossRefGoogle Scholar
  36. Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley, Hoboken (1994)CrossRefGoogle Scholar
  37. Ridder, A.: Asymptotic optimality of the cross-entropy method for Markov chain problems. Procedia Comput. Sci. 1(1), 1571–1578 (2010)CrossRefGoogle Scholar
  38. Strnadel, J.: Statistical model checking of processor systems in various interrupt scenarios. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11245, pp. 414–429. Springer, Cham (2018)CrossRefGoogle Scholar
  39. 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–215. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-27813-9_16CrossRefGoogle Scholar
  40. Sen, K., Viswanathan, M., Agha, G.A.: VESTA: a statistical model-checker and analyzer for probabilistic systems. In: QEST, pp. 251–252. IEEE Computer Society (2005)Google Scholar
  41. 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–280. Springer, Heidelberg (2005).  https://doi.org/10.1007/11513988_26CrossRefGoogle Scholar
  42. Wald, A.: Sequential tests of statistical hypotheses. Ann. Math. Stat. 16(2), 117–186 (1945)MathSciNetCrossRefGoogle Scholar
  43. White, D.J.: Real applications of Markov decision processes. Interfaces 15(6), 73–83 (1985)CrossRefGoogle Scholar
  44. White, D.J.: Further real applications of Markov decision processes. Interfaces 18(5), 55–61 (1988)MathSciNetCrossRefGoogle Scholar
  45. White, D.J.: A survey of applications of Markov decision processes. J. Oper. Res. Soc. 44(11), 1073–1096 (1993)CrossRefGoogle Scholar
  46. Younes, H.L.S.: Verification and planning for stochastic processes with asynchronous events. Ph.D. thesis, Carnegie Mellon (2005)Google Scholar
  47. Younes, H.L.S.: Ymer: a statistical model checker. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 429–433. Springer, Heidelberg (2005).  https://doi.org/10.1007/11513988_43CrossRefGoogle Scholar
  48. Zuliani, P.: Statistical model checking for biological applications. CoRR, abs/1405.2705 (2014)CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.Aalborg UniversityAalborgDenmark
  2. 2.Inria Rennes – Bretagne AtlantiqueRennesFrance

Personalised recommendations