Statistical Model Checking of Incomplete Stochastic Systems

  • Shiraj AroraEmail author
  • Axel Legay
  • Tania Richmond
  • Louis-Marie Traonouez
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11245)


We study incomplete stochastic systems that are missing some parts of their design, or are lacking information about some components. It is interesting to get early analysis results of the requirements of these systems, in order to adequately refine their design. In previous works, models for incomplete systems are analysed using model checking techniques for three-valued temporal logics. In this paper, we propose statistical model checking algorithms for these logics. We illustrate our approach on a case-study of a network system that is refined after the analysis of early designs.


  1. 1.
    Arora, S., Rao, M.V.P.: Probabilistic model checking of incomplete models. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 62–76. Springer, Cham (2016). Scholar
  2. 2.
    Arora, S., Rao, M.V.P.: Probabilistic model checking of incomplete models. CoRR abs/1706.05082 (2017)Google Scholar
  3. 3.
    Bauer, A., Leucker, M., Schallhart, C.: The good, the bad, and the ugly, but how ugly is ugly? In: Sokolsky, O., Taşıran, S. (eds.) RV 2007. LNCS, vol. 4839, pp. 126–138. Springer, Heidelberg (2007). Scholar
  4. 4.
    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). Scholar
  5. 5.
    Chechik, M., Easterbrook, S., Devereux, B.: Model checking with multi-valued temporal logics. In: Proceedings of the 31st IEEE International Symposium on Multiple-Valued Logic, pp. 187–192 (2001)Google Scholar
  6. 6.
    Chechik, M., Easterbrook, S., Petrovykh, V.: Model-checking over multi-valued logics. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol. 2021, pp. 72–98. Springer, Heidelberg (2001). Scholar
  7. 7.
    Chen, X.: Concentration inequalities for bounded random vectors. arXiv preprint: arXiv:1309.0003 (2013)
  8. 8.
    Chernoff, H.: A measure of asymptotic efficiency for tests of a hypothesis based on the sum of observations. Ann. Math. Stat. 23(4), 493–507 (1952)MathSciNetCrossRefGoogle Scholar
  9. 9.
    Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. J. ACM 42(4), 857–907 (1995)MathSciNetCrossRefGoogle Scholar
  10. 10.
    D’Argenio, P., Legay, A., Sedwards, S., Traonouez, L.: Smart sampling for lightweight verification of markov decision processes. STTT 17(4), 469–484 (2015)CrossRefGoogle Scholar
  11. 11.
    David, A., et al.: Statistical model checking for networks of priced timed automata. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol. 6919, pp. 80–96. Springer, Heidelberg (2011). Scholar
  12. 12.
    Fecher, H., Leucker, M., Wolf, V.: Don’t Know in probabilistic systems. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 71–88. Springer, Heidelberg (2006). Scholar
  13. 13.
    Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Form. Asp. Comput. 6(5), 512–535 (1994)CrossRefGoogle Scholar
  14. 14.
    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). Scholar
  15. 15.
    Huth, M., Piterman, N., Wagner, D.: Three-valued abstractions of Markov chains: completeness for a sizeable fragment of PCTL. In: Kutyłowski, M., Charatonik, W., Gębala, M. (eds.) FCT 2009. LNCS, vol. 5699, pp. 205–216. Springer, Heidelberg (2009). Scholar
  16. 16.
    Katoen, J.P., Klink, D., Leucker, M., Wolf, V.: Three-valued abstraction for probabilistic systems. J. Log. Algebr. Program. 81(4), 356–389 (2012). special Issue: NWPT 2009MathSciNetCrossRefGoogle Scholar
  17. 17.
    Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011). Scholar
  18. 18.
    Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: an overview. In: Barringer, H., et al. (eds.) RV 2010. LNCS, vol. 6418, pp. 122–135. Springer, Heidelberg (2010). Scholar
  19. 19.
    Legay, A., Sedwards, S., Traonouez, L.-M.: Plasma lab: a modular statistical model checking platform. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 77–93. Springer, Cham (2016). Scholar
  20. 20.
    Legay, A., Sedwards, S., Traonouez, L.-M.: Rare events for statistical model checking an overview. In: Larsen, K.G., Potapov, I., Srba, J. (eds.) RP 2016. LNCS, vol. 9899, pp. 23–35. Springer, Cham (2016). Scholar
  21. 21.
    Legay, A., Traonouez, L.-M.: Statistical model checking of simulink models with plasma lab. In: Artho, C., Ölveczky, P.C. (eds.) FTSCS 2015. CCIS, vol. 596, pp. 259–264. Springer, Cham (2016). Scholar
  22. 22.
    Ngo, V.C., Legay, A., Quilbeuf, J.: Statistical model checking for systemc models. In: Proceedings of HASE, pp. 197–204. IEEE Computer Society (2016)Google Scholar
  23. 23.
    Vardi, M.Y.: Automatic verification of probabilistic concurrent finite state programs. In: Proceedings of SFCS, pp. 327–338. IEEE Computer Society (1985)Google Scholar
  24. 24.
    Wald, A.: Sequential tests of statistical hypotheses. Ann. Math. Stat. 16(2), 117–186 (1945)MathSciNetCrossRefGoogle Scholar
  25. 25.
    Younes, H.L.S.: Verification and Planning for Stochastic Processes with Asynchronous Events. Ph.D. thesis, Carnegie Mellon (2005)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  • Shiraj Arora
    • 1
    Email author
  • Axel Legay
    • 2
  • Tania Richmond
    • 2
  • Louis-Marie Traonouez
    • 2
  1. 1.Indian Institute of Technology HyderabadHyderabadIndia
  2. 2.InriaRennesFrance

Personalised recommendations