Skip to main content
SpringerLink
Log in
Book cover

International Symposium on Leveraging Applications of Formal Methods

ISoLA 2018: Leveraging Applications of Formal Methods, Verification and Validation. Verification pp 261–270Cite as

Statistical Model Checking the 2018 Edition!

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNTCS,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.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

References

  • 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)

    Google Scholar 

  • 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)

    Google Scholar 

  • 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)

    Article  Google Scholar 

  • 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 

  • 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)

    Google Scholar 

  • 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_12

    Chapter  Google Scholar 

  • 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_70

    Chapter  MATH  Google Scholar 

  • 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 

  • Bellman, R.: Dynamic Programming. Princeton University Press, Princeton (1957)

    MATH  Google Scholar 

  • 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_4

    Chapter  Google Scholar 

  • Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for continuous-time Markov chains. IEEE 29(6), 524–541 (2003)

    MATH  Google Scholar 

  • 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_23

    Chapter  MATH  Google Scholar 

  • 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 

  • Clarke, E.M., Emerson, E.A., Sifakis, J.: Model checking: algorithmic verification and debugging. Commun. ACM 52(11), 74–84 (2009)

    Article  Google Scholar 

  • 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_5

    Chapter  Google Scholar 

  • Cérou, F., Guyader, A.: Adaptive multilevel splitting for rare event analysis. Stoch. Anal. Appl. 25, 417–443 (2007)

    Article  MathSciNet  Google Scholar 

  • 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_1

    Chapter  MATH  Google Scholar 

  • 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 

  • 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_24

    Chapter  Google Scholar 

  • 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)

    Google Scholar 

  • David, A., Jensen, P.G., Larsen, K.G., Legay, A., Lime, D., Sorensen, M.G., Taankvist, J.H

    Google Scholar 

  • 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)

    Google Scholar 

  • 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_27

    Chapter  Google Scholar 

  • 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)

    Google Scholar 

  • Hermanns, H., Hartmanns, A.: An internet inspired approach to power grid stability. IT Inf. Technol. 55(2), 45–51 (2013)

    Google Scholar 

  • 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_8

    Chapter  MATH  Google Scholar 

  • 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 

  • 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_23

    Chapter  Google Scholar 

  • 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_26

    Chapter  Google Scholar 

  • 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_38

    Chapter  Google Scholar 

  • Kahn, H., Marshall, A.W.: Methods of reducing sample size in Monte Carlo computations. Oper. Res. 1(5), 263–278 (1953)

    MATH  Google Scholar 

  • 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 

  • Guldstrand Larsen, K., Skou, A., Kim Guldstrand Larsen and Arne Skou: Bisimulation through probabilistic testing. Inf. Comput. 94(1), 1–28 (1991)

    Article  MathSciNet  Google Scholar 

  • Legay, A., Sedwards, S.: Lightweight Monte Carlo verification of Markov decision processes (2014, submitted)

    Google Scholar 

  • Okamoto, M.: Some inequalities relating to the partial sum of binomial probabilities. Ann. Inst. Stat. Math. 10, 29–35 (1959)

    Article  MathSciNet  Google Scholar 

  • Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley, Hoboken (1994)

    Book  Google Scholar 

  • Ridder, A.: Asymptotic optimality of the cross-entropy method for Markov chain problems. Procedia Comput. Sci. 1(1), 1571–1578 (2010)

    Article  Google Scholar 

  • 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)

    Google Scholar 

  • 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_16

    Chapter  Google Scholar 

  • 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 

  • 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_26

    Chapter  Google Scholar 

  • Wald, A.: Sequential tests of statistical hypotheses. Ann. Math. Stat. 16(2), 117–186 (1945)

    Article  MathSciNet  Google Scholar 

  • White, D.J.: Real applications of Markov decision processes. Interfaces 15(6), 73–83 (1985)

    Article  Google Scholar 

  • White, D.J.: Further real applications of Markov decision processes. Interfaces 18(5), 55–61 (1988)

    Article  Google Scholar 

  • White, D.J.: A survey of applications of Markov decision processes. J. Oper. Res. Soc. 44(11), 1073–1096 (1993)

    Article  Google Scholar 

  • Younes, H.L.S.: Verification and planning for stochastic processes with asynchronous events. Ph.D. thesis, Carnegie Mellon (2005)

    Google Scholar 

  • 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_43

    Chapter  Google Scholar 

  • Zuliani, P.: Statistical model checking for biological applications. CoRR, abs/1405.2705 (2014)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Aalborg University, Aalborg, Denmark

    Kim Guldstrand Larsen & Axel Legay

  2. Inria Rennes – Bretagne Atlantique, Rennes, France

    Kim Guldstrand Larsen & Axel Legay

Authors
  1. Kim Guldstrand Larsen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Axel Legay
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Kim Guldstrand Larsen .

Editor information

Editors and Affiliations

  1. University of Limerick, Limerick, Ireland

    Tiziana Margaria

  2. TU Dortmund, Dortmund, Germany

    Bernhard Steffen

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Guldstrand Larsen, K., Legay, A. (2018). Statistical Model Checking the 2018 Edition!. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation. Verification. ISoLA 2018. Lecture Notes in Computer Science(), vol 11245. Springer, Cham. https://doi.org/10.1007/978-3-030-03421-4_17

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-03421-4_17

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-03420-7

  • Online ISBN: 978-3-030-03421-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation