Probabilistic Model Checking of Incomplete Models | SpringerLink
Skip to main content
Springer Nature Link
Log in

Probabilistic Model Checking of Incomplete Models

  • Conference paper
  • First Online:
Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques (ISoLA 2016)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9952))

Included in the following conference series:

Abstract

It is crucial for accurate model checking that the model be a complete and faithful representation of the system. Unfortunately, this is not always possible, mainly because of two reasons: (i) the model is still under development and (ii) the correctness of implementation of some modules is not established. In such circumstances, is it still possible to get correct answers for some model checking queries?

This paper is a step towards answering this question. We formulate the problem for the Discrete Time Markov Chains (DTMC) modeling formalism and the Probabilistic Computation Tree Logic (PCTL) query language. We then propose a simple solution by modifying DTMC and PCTL to accommodate three valued logic. The technique builds on existing model checking algorithms and tools, obviating the need for new ones to account for three valued logic. Finally, we provide an experimental demonstration of our approach.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 11439
Price includes VAT (Japan)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 14299
Price includes VAT (Japan)
  • 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

Institutional subscriptions

Similar content being viewed by others

References

  1. AlTurki, M., Meseguer, J.: PVeStA: a parallel statistical model checking and quantitative analysis tool. In: Corradini, A., Klin, B., Cîrstea, C. (eds.) CALCO 2011. LNCS, vol. 6859, pp. 386–392. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22944-2_28

    Chapter  Google Scholar 

  2. Baier, C., Haverkort, B., Hermanns, H., Katoen, J.P.: Model-checking algorithms for continuous-time markov chains. IEEE Trans. Software Eng. 29(6), 524–541 (2003)

    Article  MATH  Google Scholar 

  3. Baier, C., Katoen, J.P.: Principles of Model Checking (Representation and Mind Series). The MIT Press, Cambridge (2008)

    MATH  Google Scholar 

  4. Bruns, G., Godefroid, P.: Model checking partial state spaces with 3-valued temporal logics. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol. 1633, pp. 274–287. Springer, Heidelberg (1999). doi:10.1007/3-540-48683-6_25

    Chapter  Google Scholar 

  5. Bruns, G., Godefroid, P.: Generalized model checking: reasoning about partial state spaces. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 168–182. Springer, Heidelberg (2000). doi:10.1007/3-540-44618-4_14

    Chapter  Google Scholar 

  6. Caillaud, B., Delahaye, B., Larsen, K.G., Legay, A., Pedersen, M.L., Wsowski, A.: Constraint markov chains. Theoret. Comput. Sci. 412(34), 4373–4404 (2011). http://www.sciencedirect.com/science/article/pii/S0304397511003926

    Article  MathSciNet  MATH  Google Scholar 

  7. Chechik, M.: On interpreting results of model-checking with abstraction. University of Toronto, Technical report (2000)

    Google Scholar 

  8. 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). doi:10.1007/3-540-45251-6_5

    Chapter  Google Scholar 

  9. Courcoubetis, C., Yannakakis, M.: Verifying temporal properties of finite-state probabilistic programs. In: 1988, 29th Annual Symposium on Foundations of Computer Science, pp. 338–345. IEEE (1988)

    Google Scholar 

  10. Delahaye, B., Katoen, J.P., Larsen, K.G., Legay, A., Pedersen, M.L., Sher, F., Wsowski, A.: Abstract probabilistic automata. Inf. Comput. 232, 66–116 (2013). http://www.sciencedirect.com/science/article/pii/S0890540113001132

    Article  MathSciNet  MATH  Google Scholar 

  11. 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). doi:10.1007/11691617_5

    Chapter  Google Scholar 

  12. Godefroid, P., Piterman, N.: LTL generalized model checking revisited. Int. J. Softw. Tools Technol. Transfer 13(6), 571–584 (2011)

    Article  MATH  Google Scholar 

  13. Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Asp. Comput. 6(5), 512–535 (1994). http://dx.doi.org/10.1007/BF01211866

    Article  MATH  Google Scholar 

  14. 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). doi:10.1007/978-3-642-03409-1_19

    Chapter  Google Scholar 

  15. Klink, D.: Three-Valued Abstraction for Stochastic Systems. Verlag Dr. Hut, Munich (2010)

    Google Scholar 

  16. 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). doi:10.1007/978-3-642-22110-1_47

    Chapter  Google Scholar 

  17. Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: an overview. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Roşu, G., Sokolsky, O., Tillmann, N. (eds.) RV 2010. LNCS, vol. 6418, pp. 122–135. Springer, Heidelberg (2010). doi:10.1007/978-3-642-16612-9_11

    Chapter  Google Scholar 

  18. Malinowski, G.: Many-Valued Logics. Clarendon Press, Oxford (1993)

    MATH  Google Scholar 

  19. Putnam, H.: Three-valued logic. Philos. Stud. 8(5), 73–80 (1957)

    Article  MathSciNet  Google Scholar 

  20. Rescher, N.: Many-Valued Logic. Springer, Netherlands (1968)

    Book  MATH  Google Scholar 

  21. Sebastio, S., Vandin, A.: Multivesta: statistical model checking for discrete event simulators. In: 7th International Conference on Performance Evaluation Methodologies and Tools, ValueTools 2013, Torino, Italy, December 10–12, 2013, pp. 310–315 (2013)

    Google Scholar 

  22. Sen, K., Viswanathan, M., Agha, G.A.: VESTA: a statistical model-checker and analyzer for probabilistic systems. In: Second International Conference on the Quantitative Evaluation of Systems (QEST 2005), 19–22, September 2005, Torino, Italy, pp. 251–252 (2005)

    Google Scholar 

  23. Younes, H.L.S., Kwiatkowska, M.Z., Norman, G., Parker, D.: Numerical vs. statistical probabilistic model checking: an empirical study. In: Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference on TACAS 2004, Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, 29 March–2 April, 2004, Proceedings, pp. 46–60 (2004)

    Google Scholar 

  24. Younes, H.L.S., Simmons, R.G.: Probabilistic verification of discrete event systems using acceptance sampling. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 223–235. Springer, Heidelberg (2002). doi:10.1007/3-540-45657-0_17

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Indian Institute of Technology Hyderabad, Hyderabad, India

    Shiraj Arora & M. V. Panduranga Rao

Authors
  1. Shiraj Arora
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. M. V. Panduranga Rao
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to M. V. Panduranga Rao .

Editor information

Editors and Affiliations

  1. Lero, Limerick, Ireland

    Tiziana Margaria

  2. TU Dortmund, Dortmund, Germany

    Bernhard Steffen

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing AG

About this paper

Cite this paper

Arora, S., Rao, M.V.P. (2016). Probabilistic Model Checking of Incomplete Models. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques. ISoLA 2016. Lecture Notes in Computer Science(), vol 9952. Springer, Cham. https://doi.org/10.1007/978-3-319-47166-2_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-47166-2_5

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-47165-5

  • Online ISBN: 978-3-319-47166-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation