Skip to main content
SpringerLink
Log in

Efficient Probabilistic Model Checking on General Purpose Graphics Processors

  • Conference paper
Model Checking Software (SPIN 2009)

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

Included in the following conference series:

Abstract

We present algorithms for parallel probabilistic model checking on general purpose graphic processing units (GPGPUs). For this purpose we exploit the fact that some of the basic algorithms for probabilistic model checking rely on matrix vector multiplication. Since this kind of linear algebraic operations are implemented very efficiently on GPGPUs, the new parallel algorithms can achieve considerable runtime improvements compared to their counterparts on standard architectures. We implemented our parallel algorithms on top of the probabilistic model checker PRISM. The prototype implementation was evaluated on several case studies in which we observed significant speedup over the standard CPU implementation of the tool.

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

Access this chapter

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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Allmaier, S.C., Kowarschik, M., Horton, G.: State Space Construction and Steady-state Solution of GSPNs on a Shared-Memory Multiprocessor. In: Proc. 7th Int. Workshop on Petri Nets and Peformance Models (PNPM 1997), pp. 112–121. IEEE Comp. Soc. Press, Los Alamitos (1997)

    Google Scholar 

  2. Baier, C., Katoen, J.-P.: Principles of Model Checking, p. 950. MIT Press, Cambridge (2008)

    MATH  Google Scholar 

  3. Baier, C., Katoen, J.-P., Hermanns, H., Haverkort, B.: Model-Checking Algorithms for Contiuous-Time Markov Chains. IEEE Transactions on Software Engineering 29(6), 524–541 (2003)

    Article  Google Scholar 

  4. Bal, H., Barnat, J., Brim, L., Verstoep, K.: Efficient Large-Scale Model Checking. In: IEEE International Parallel & Distributed Processing Symposium (IPDPS) (to appear, 2009)

    Google Scholar 

  5. Barnat, J., Brim, L., Ročkai, P.: Scalable Multi-core Model-Checking. In: Bošnački, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 187–203. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  6. Barnat, J., Brim, L., Černá, I., Ceska, M., Tumova, J.: ProbDiVinE-MC: Multi-core LTL Model Checker for Probabilistic Systems. In: International Conference on the Quantitative Evaluaiton of Systems QEST 2008, pp. 77–78. IEEE Compuer Society Press, Los Alamitos (2008)

    Chapter  Google Scholar 

  7. Barnat, J., Brim, L., Šimeček, P.: I/O efficient accepting cycle detection. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 281–293. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  8. Barnat, J., Brim, L., Stríbrná, J.: Distributed LTL Model Checking in SPIN. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 200–216. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  9. Barnat, J., Brim, L., Šimeček, P., Weber, M.: Revisiting resistance speeds up I/O-efficient LTL model checking. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 48–62. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  10. Baskaran, M.M., Bordawekar, R.: Optimzing Sparse Matrix-Vector Multiplication on GPUs Using Compile-time and Run-time Strategies, IBM Reserach Report, RC24704, W0812-047 (2008)

    Google Scholar 

  11. Bell, A., Haverkort, B.R.: Distribute Disk-based Algorithms for Model Checking Very Large Markov Chains. In: Formal Methods in System Design, vol. 29, pp. 177–196. Springer, Heidelberg (2006)

    Google Scholar 

  12. Ciardo, G.: Distributed and Structured Analysis Approaches to Study Large and Complex Systems. European Educational Forum: School on Formal Methods and Performance Analysis 2000, 344–374 (2000)

    MATH  Google Scholar 

  13. Dai, P., Mausam, Weld, D.S.: External Memory Value Iteration. In: Proc. of the Twenty-Third AAAI Conf. on Artificial Intelligence (AAAI), pp. 898–904 (2008)

    Google Scholar 

  14. http://www.nvidia.com/object/cuda_home.html#

  15. Edelkamp, S., Sulewski, D.: Model Checking via Delayed Duplicate Detection on the GPU, Technical Report 821, Universität Dortmund, Fachberich Informatik, ISSN 0933-6192 (2008)

    Google Scholar 

  16. Edelkamp, S., Jabbar, S.: Large-scale directed model checking LTL. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 1–18. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  17. Edelkamp, S., Jabbar, S., Bonet, B.: External Memory Value Iteration. In: Proc. 17th Int. Conf. on Automated Planning and Scheduling, pp. 128–135. AAAI Press, Menlo Park (2007)

    Google Scholar 

  18. Edelkamp, S., Sanders, P., Šimeček, P.: Semi-external LTL model checking. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 530–542. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  19. Edelkamp, S., Sulewski, D.: Flash-efficient LTL model checking with minimal counterexamples. In: Software Engineering and Formal Methods, pp. 73–82 (2008)

    Google Scholar 

  20. Hansson, H., Jonsson, B.: A Logic for reasoning about time and reliability. Formal Aspects of Computing 6(5), 512–535 (1994)

    Article  MATH  Google Scholar 

  21. Haverkort, B., Hermanns, H., Katoen, J.-P.: On the Use of Model Checking Techniques for Dependability Evaluation. In: Proc. 19th IEEE Symposium on Reliable Distributed Systems (SRDS 2000), pp. 228–237 (2000)

    Google Scholar 

  22. Herman, T.: Probabilistic Self-stabilization. Information Processing Letters 35(2), 63–67 (1990)

    Article  MathSciNet  MATH  Google Scholar 

  23. Hermanns, H., Meyer-Kayser, J., Siegle, M.: Multi Terminal Binary Decision Diagrams to Represent and Analyse Continuous Time Markov Chains. In: Proc. 3rd International Workshop on Numerical Solution of Markov Chains (NSMC 1999), pp. 188–207 (1999)

    Google Scholar 

  24. Holzmann, G.J., Bošnački, D.: The Design of a multi-core extension of the Spin Model Checker. IEEE Trans. on Software Engineering 33(10), 659–674 (2007); (first presented at: Formal Methods in Computer Aided Design (FMCAD), San Jose (November 2006))

    Article  Google Scholar 

  25. Holzmann, G.J., Bošnački, D.: Multi-core Model Checking with Spin. In: Proc. Parallel and Distributed Processing Symposium, IPDPS 2007, IEEE International, pp. 1–8 (2007)

    Google Scholar 

  26. Inggs, C.P., Barringer, H.: CTL* Model Checking on a Shared Memory Architecture. Electronic Notes in Theoretical Computer Science 128(4), 107–123 (2005)

    Article  MATH  Google Scholar 

  27. Inggs, C.P., Barringer, H.: Effective State Exploration for Model Checking on a Shared Memory Architecture. Electronic Notes in Theoretical Computer Science 68(4) (2002)

    Google Scholar 

  28. Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM: Probabilistic Symbolic Model Checker. In: Field, T., Harrison, P.G., Bradley, J., Harder, U. (eds.) TOOLS 2002. LNCS, vol. 2324, pp. 200–204. Springer, Heidelberg (2002)

    Google Scholar 

  29. Kwiatkowska, M., Norman, G., Parker, D.: Stochastic Model Checking. In: Bernardo, M., Hillston, J. (eds.) SFM 2007. LNCS, vol. 4486, pp. 220–270. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  30. Lerda, F., Sisto, R.: Distributed Model Checking in SPIN. In: Dams, D.R., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol. 1680, pp. 22–39. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  31. Marowka, A.: Parallel Computing on Any Desktop. Comm. of the ACM 50(9), 75–78 (2007)

    Article  Google Scholar 

  32. Philips, J.C., Braun, R., Wang, W., Gumbart, J., Tajkhorshid, E., Villa, E., Chipot, C., Skeel, R.D., Kale, L., Sculten, K.: Scalable Molecular Dynamics with NAMD. Journal of Computational Chemistry 26, 1781–1802 (2005)

    Article  Google Scholar 

  33. Stern, U., Dill, D.: Parallelizing the Murφ Verifier. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 256–278. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  34. Stewart, W.J.: Introduction to the Numerical Solution of Markov Chains. Princeton University Press, Princeton (1994)

    MATH  Google Scholar 

  35. Valmari, A.: The State Explosion Problem. In: Reisig, W., Rozenberg, G. (eds.) APN 1998. LNCS, vol. 1491, pp. 429–528. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Eindhoven University of Technology, The Netherlands

    Dragan Bošnački

  2. TZI, Universität Bremen, Germany

    Stefan Edelkamp

  3. Technische Universität Dortmund, Germany

    Damian Sulewski

Authors
  1. Dragan Bošnački
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Stefan Edelkamp
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Damian Sulewski
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Space Science Division, NASA Ames Research Center, Mail Stop 269-2, 94035, Moffett Field, CA, USA

    Corina S. Păsăreanu

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bošnački, D., Edelkamp, S., Sulewski, D. (2009). Efficient Probabilistic Model Checking on General Purpose Graphics Processors. In: Păsăreanu, C.S. (eds) Model Checking Software. SPIN 2009. Lecture Notes in Computer Science, vol 5578. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02652-2_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-02652-2_7

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-02651-5

  • Online ISBN: 978-3-642-02652-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation