Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

A Design of GPU-Based Quantitative Model Checking

  • Conference paper
  • First Online:
Verification, Model Checking, and Abstract Interpretation (VMCAI 2021)

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

Abstract

In this paper, we implement a GPU-based quantitative model checker and compare its performance with a CPU-based one. Linear Temporal Logic for Control (LTLC) is a quantitative variation of LTL to describe properties of a linear system and LTLC-Checker [1] is an implementation of its model checking algorithm. In practice, its long and unpredictable execution time has been a concern in applying the technique to real-time applications such as automatic control systems. In this paper, we design an LTLC model checker using a GPGPU programming technique. The resulting model checker is not only faster than the CPU-based one especially when the problem is not simple, but it has less variation in the execution time as well. Furthermore, multiple counterexamples can be found together when the CPU-based checker can find only one.

Y. Kwon—This work was supported by NRF of MSIT, Korea (2019R1F1A1058770).

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
$34.99 /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
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 79.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 99.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

Similar content being viewed by others

Notes

  1. 1.

    To distinguish with other queues, we call the queue for the BFS a BFS queue or a BFS-Q.

  2. 2.

    The terms beginning with capital letters like Task and DevTask represent types and those beginning with small letters like task and devTask represent their instances.

References

  1. LTLC-GPU. http://www3.cs.stonybrook.edu/~youngkwon/sw/LTLCCuda.v0.8.190224.zip

  2. Ahamed, A.K.C., Magoulès, F.: Parallel sub-structuring methods for solving sparse linear systems on a cluster of GPUs. In: 2014 IEEE International Conference on High Performance Computing and Communications, 2014 IEEE 6th International Symposium on Cyberspace Safety and Security, 2014 IEEE 11th International Conference on Embedded Software and System (HPCC, CSS, ICESS), pp. 121–128. IEEE (2014)

    Google Scholar 

  3. Ahamed, A.K.C., Magoulès, F.: GPU accelerated substructuring methods for sparse linear systems. In: 2016 IEEE International Conference on Computational Science and Engineering (CSE) and IEEE International Conference on Embedded and Ubiquitous Computing (EUC) and 15th International Symposium on Distributed Computing and Applications for Business Engineering (DCABES), pp. 614–625. IEEE (2016)

    Google Scholar 

  4. Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126, 183–235 (1994)

    Article  MathSciNet  Google Scholar 

  5. Banterle, F., Giacobazzi, R.: A fast implementation of the octagon abstract domain on graphics hardware. In: Nielson, H.R., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 315–332. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-74061-2_20

    Chapter  Google Scholar 

  6. Barnat, J., Bauch, P., Brim, L., Ceska, M.: Employing multiple CUDA devices to accelerate LTL model checking. In: 2010 IEEE 16th International Conference on Parallel and Distributed Systems, pp. 259–266. IEEE (2010)

    Google Scholar 

  7. Bartocci, E., DeFrancisco, R., Smolka, S.A.: Towards a GPGPU-parallel SPIN model checker. In: International SPIN Symposium on Model Checking of Software, pp. 87–96. ACM (2014)

    Google Scholar 

  8. Bu, L., Li, Y., Wang, L., Li, X.: BACH: bounded reachability checker for linear hybrid automata. In: Formal Methods in Computer Aided Design, pp. 65–68. IEEE Computer Society (2008)

    Google Scholar 

  9. Büchi, J.: On a decision method in restricted second order arithmetic. In: Proceedings of the International Conference on Logic, Methodology and Philosophy of Science, pp. 1–11. Stanford University Press (1960)

    Google Scholar 

  10. Clarke, D., Mohtai, C., Tuffs, P.: Generalized predictive control. Automatica 23, 137–160 (1987)

    Article  Google Scholar 

  11. Clarke, D., Scattolini, R.: Constrained receding-horizon predictive control. In: IEE Proceedings Part D, vol. 138, pp. 347–354 (1991)

    Google Scholar 

  12. Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)

    Google Scholar 

  13. Franklin, G.F., Powell, J.D., Emami-Naeini, A.: Feedback control of dynamic systems, vol. 3 (2002)

    Google Scholar 

  14. Fränzle, M., Herde, C.: HySAT: an efficient proof engine for bounded model checking of hybrid systems. Formal Methods Syst. Des. 30, 179–198 (2007)

    Article  Google Scholar 

  15. Girard, A., Pola, G., Tabuada, P.: Approximately bisimilar symbolic models for incrementally stable switched systems. Trans. Autom. Control 55, 116–126 (2010)

    Article  MathSciNet  Google Scholar 

  16. Henzinger, T.A.: The theory of hybrid automata. In: Annual Symposium on Logic in Computer Science, pp. 278–292. IEEE Computer Society (1996)

    Google Scholar 

  17. Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: HyTech: a model checker for hybrid systems. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 460–463. Springer, Heidelberg (1997). https://doi.org/10.1007/3-540-63166-6_48

    Chapter  Google Scholar 

  18. Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23, 279–295 (1997)

    Article  Google Scholar 

  19. Holzmann, G.J.: Parallelizing the spin model checker. In: Donaldson, A., Parker, D. (eds.) SPIN 2012. LNCS, vol. 7385, pp. 155–171. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31759-0_12

    Chapter  Google Scholar 

  20. Karmarkar, N.: A new polynomial-time algorithm for linear programming. In: Combinatorica, vol. 4, pp. 373–395 (1984)

    Google Scholar 

  21. Khun, J., Šimeček, I., Lórencz, R.: GPU solver for systems of linear equations with infinite precision. In: 2015 17th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), pp. 121–124. IEEE (2015)

    Google Scholar 

  22. Kloetzer, M., Belta, C.: A fully automated framework for control of linear systems from temporal logic specifications. Trans. Autom. Control 53, 287–297 (2008)

    Article  MathSciNet  Google Scholar 

  23. Kwon, Y.M., Agha, G.: LTLC: linear temporal logic for control. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol. 4981, pp. 316–329. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78929-1_23

    Chapter  Google Scholar 

  24. Kwon, Y., Kim, E.: Bounded model checking of hybrid systems for control. IEEE Trans. Autom. Control 60, 2961–2976 (2015)

    Article  MathSciNet  Google Scholar 

  25. Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Int. J. Softw. Tools Technol. Transf. 1, 134–152 (1997)

    Article  Google Scholar 

  26. Law, A.M., Kelton, W.D.: Simulation Modeling & Analysis. McGraw-Hill, New York (1991)

    Google Scholar 

  27. Lichtenstein, O., Pnueli, A.: Checking that finite state concurrent programs satisfy their linear specification. In: POPL, pp. 97–107 (1985)

    Google Scholar 

  28. Liu, J., Ozay, N., Topcu, U., Murray, R.M.: Synthesis of reactive switching protocols from temporal logic specifications. Trans. Autom. Control 58(7), 1771–1785 (2013)

    Article  MathSciNet  Google Scholar 

  29. Luenberger, D.G.: Linear and Nonlinear Programming, 2nd edn. Addison Wesley, Boston (1989)

    Google Scholar 

  30. McClanahan, C.: History and evolution of GPU architecture. A Survey Paper, p. 9 (2010)

    Google Scholar 

  31. Miné, A.: The octagon abstract domain. In: Proceedings Eighth Working Conference on Reverse Engineering, pp. 310–319. IEEE (2001)

    Google Scholar 

  32. Ramanathan, R.: Intel multi-core processors: making the move to quad-core and beyond. Technology@ Intel Mag. 4(9), 2–4 (2006)

    Google Scholar 

  33. Venu, B.: Multi-core processors-an overview. arXiv preprint arXiv:1110.3535 (2011)

  34. Wijs, A.: BFS-based model checking of linear-time properties with an application on GPUs. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 472–493. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41540-6_26

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, The State University of New York, Incheon, Korea

    YoungMin Kwon

  2. 2e Consulting Corporation, Seoul, South Korea

    Eunhee Kim

Authors
  1. YoungMin Kwon
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Eunhee Kim
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to YoungMin Kwon .

Editor information

Editors and Affiliations

  1. University of Copenhagen, Copenhagen, Denmark

    Fritz Henglein

  2. Tel Aviv University, Tel Aviv, Israel

    Sharon Shoham

  3. Technion, Haifa, Israel

    Yakir Vizel

Rights and permissions

Reprints and permissions

Copyright information

© 2021 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Kwon, Y., Kim, E. (2021). A Design of GPU-Based Quantitative Model Checking. In: Henglein, F., Shoham, S., Vizel, Y. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2021. Lecture Notes in Computer Science(), vol 12597. Springer, Cham. https://doi.org/10.1007/978-3-030-67067-2_20

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-67067-2_20

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-67066-5

  • Online ISBN: 978-3-030-67067-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation