Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Model Checking Algorithms for Hyperproperties (Invited Paper) Kapitel lesen Erstes Kapitel lesen

2021 | OriginalPaper | Buchkapitel

A Design of GPU-Based Quantitative Model Checking

verfasst von : YoungMin Kwon, Eunhee Kim

Erschienen in: Verification, Model Checking, and Abstract Interpretation

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Vorheriges Kapitel A Synchronous Effects Logic for Temporal Verification of Pure Esterel
Nächstes Kapitel Formal Semantics and Verification of Network-Based Biocomputation Circuits
Fußnoten
1
To distinguish with other queues, we call the queue for the BFS a BFS queue or a BFS-Q.
 
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.
 
Literatur
1.
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)
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)
4.
5.
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)
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)
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)
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)
10.
Clarke, D., Mohtai, C., Tuffs, P.: Generalized predictive control. Automatica 23, 137–160 (1987)CrossRef
11.
Clarke, D., Scattolini, R.: Constrained receding-horizon predictive control. In: IEE Proceedings Part D, vol. 138, pp. 347–354 (1991)
12.
Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)MATH
13.
Franklin, G.F., Powell, J.D., Emami-Naeini, A.: Feedback control of dynamic systems, vol. 3 (2002)
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)CrossRef
15.
Girard, A., Pola, G., Tabuada, P.: Approximately bisimilar symbolic models for incrementally stable switched systems. Trans. Autom. Control 55, 116–126 (2010)MathSciNetCrossRef
16.
Henzinger, T.A.: The theory of hybrid automata. In: Annual Symposium on Logic in Computer Science, pp. 278–292. IEEE Computer Society (1996)
17.
18.
Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23, 279–295 (1997)CrossRef
19.
20.
Karmarkar, N.: A new polynomial-time algorithm for linear programming. In: Combinatorica, vol. 4, pp. 373–395 (1984)
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)
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)MathSciNetCrossRef
23.
24.
Kwon, Y., Kim, E.: Bounded model checking of hybrid systems for control. IEEE Trans. Autom. Control 60, 2961–2976 (2015)MathSciNetCrossRef
25.
Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Int. J. Softw. Tools Technol. Transf. 1, 134–152 (1997)CrossRef
26.
Law, A.M., Kelton, W.D.: Simulation Modeling & Analysis. McGraw-Hill, New York (1991)MATH
27.
Lichtenstein, O., Pnueli, A.: Checking that finite state concurrent programs satisfy their linear specification. In: POPL, pp. 97–107 (1985)
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)MathSciNetCrossRef
29.
Luenberger, D.G.: Linear and Nonlinear Programming, 2nd edn. Addison Wesley, Boston (1989)MATH
30.
McClanahan, C.: History and evolution of GPU architecture. A Survey Paper, p. 9 (2010)
31.
Miné, A.: The octagon abstract domain. In: Proceedings Eighth Working Conference on Reverse Engineering, pp. 310–319. IEEE (2001)
32.
Ramanathan, R.: Intel multi-core processors: making the move to quad-core and beyond. Technology@ Intel Mag. 4(9), 2–4 (2006)
33.
34.
Metadaten
Titel
A Design of GPU-Based Quantitative Model Checking
verfasst von
YoungMin Kwon
Eunhee Kim
Copyright-Jahr
2021
Buch
Verification, Model Checking, and Abstract Interpretation

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

Electronic ISBN: 978-3-030-67067-2

Copyright-Jahr: 2021

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