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
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
MTZ-Fachkongress

Antriebe und Energiesysteme von morgen


Austausch von Automobil- und Energiewirtschaft

Am 14./15. Mai geht es in Chemnitz um die Mobilitätswende durch Elektro- und Wasserstofffahrzeuge.
Erweiterte Suche
Anmelden
nach oben
International Journal on Software Tools for Technology Transfer
Erschienen in: International Journal on Software Tools for Technology Transfer 2/2016

01.04.2016 | TACAS 2014

Concurrent depth-first search algorithms based on Tarjan’s Algorithm

verfasst von: Gavin Lowe

Erschienen in: International Journal on Software Tools for Technology Transfer | Ausgabe 2/2016

Einloggen

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

search-config
loading …

Abstract

We present concurrent algorithms, based on depth-first search, for three problems relevant to model checking: given a state graph, to find its strongly connected components, which states are in loops, and which states are in “lassos”. Each algorithm is a variant of Tarjan’s Algorithm. Our algorithms typically exhibit a three- or four-fold speed-up over the corresponding sequential algorithms on an eight-core machine.
Vorheriger Artikel Some recent advances in automated analysis
Nächster Artikel FDR3: a parallel refinement checker for CSP

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
Anhänge
Nur mit Berechtigung zugänglich
Fußnoten
Literatur
1.
Armstrong, P., Lowe, G., Ouaknine, J., Roscoe, A.W.: Model checking timed CSP. In: Proceedings of HOWARD-60 (2012)
2.
Barnat, J., Chaloupka, J., van de Pol, J.: Distributed algorithms for SCC decomposition. J. Logic Comput. 21(1), 23–44 (2011)MathSciNetCrossRefMATH
3.
4.
Courcoubetis, C., Vardi, M. Y., Wolper, P., Yannakakis, M.: Memory efficient algorithms for the verification of temporal properties. In: Proceedings of Computer-Aided Verification (CAV), vol. 531 of LNCS, pp. 233–242 (1990)
5.
6.
Evangelista, S., Laarman, A.W., Petrucci, L., van de Pol, J.C.: Improved multi-core nested depth-first search. In: Proceedings of the 10th International Symposium on Automated Technology for Verification and Analysis, vol. 7561 of Lecture Notes in Computer Science, pp. 269–283 (2012)
7.
Evangelista, S., Petrucci, L., Youcef, S.: Parallel nested depth-first searches for LTL model checking. In: Proceedings of the 9th International Symposium on Automated Technology for Verification and Analysis, vol. 6996 of Lecture Notes in Computer Science, pp. 381–396 (2011)
8.
Fleischer, L.K., Hendrickson, B., Pnar, A.: On identifying strongly connected components in parallel. In: Parallel and Distributed Processing, vol. 1800 of Lecture Notes in Computer Science, pp. 505–511 (2000)
9.
10.
Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3–a modern refinement checker for CSP. In: Proceedings of Tools and Algorithms for the Construction and Analysis of Systems (TACAS), vol. 8413 of Lecture Notes in Computer Science, pp. 187–201 (2014)
11.
Holzmann, G.J., Bos̆nac̆ki, D.: Multi-core model checking with spin. In: Proceedings of Parallel and Distributed Processing Symposium, pp. 1–8 (2007)
12.
Laarman, A., van de Pol, J., Weber, M.: Boosting multi-core reachability performance with shared hash tables. In: Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2010) (2010)
13.
Laarman, A.W., Langerak, R., van de Pol, J.C., Weber, M., Wijs, A.: Multi-core nested depth-first search. In: Proceedings of the 9th International Symposium on Automated Technology for Verification and Analysis, vol. 6996 of Lecture Notes in Computer Science, pp. 321–335 (2011)
14.
Laarman, A.W., van de Pol, J.C.: Variations on multi-core nested depth-first search. In: Proceedings of the 10th International Workshop on Parallel and Distributed Methods in Verification, vol. 72 of Electronic Proceedings in Theoretical Computer Science, pp. 13–28 (2011)
15.
Lowe, G.: Implementing generalised alt: a case study in validated design using CSP. In: Communicating Process Architectures (2011)
16.
Lowe, G.: Concurrent hash maps: a comparative study. Technical report, University of Oxford (2014)
17.
McLendon III, W., Hendrickson, B., Plimpton, S.J., Rauchwerger, L.: Finding strongly connected components in distributed graphs. J.Parallel Distrib. Comput. 65(8), 901–910 (2005)CrossRefMATH
18.
Odersky, M., Spoon, L., Venners, B.: Programming in Scala. Artima (2008)
19.
Orzan, S.: On Distributed Verification and Verified Distribution. Ph.D. thesis, Free University of Amsterdam (2004)
20.
21.
Renault, E., Duret-Lutz, A., Kordon, F., Poitrenaud, D.: Parallel explicit model checking for generalized Büchi automata. In: Proceedings of Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (2015) (Forthcoming)
22.
Roscoe, A.W.: Theory and Practice of Concurrency. Prentice Hall, Europe (1998)
23.
24.
25.
Tomkins, D., Smith, T.G., Amato, N.M., Rauchwerger, L.: SCCMulti: an improved parallel strongly connected components algorithm. In: Proceedings of the ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP ’14) (2014)
26.
27.
Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proceedings of Logic in Computer Science (1986)
Metadaten
Titel
Concurrent depth-first search algorithms based on Tarjan’s Algorithm
verfasst von
Gavin Lowe
Publikationsdatum
01.04.2016
Verlag
Springer Berlin Heidelberg
Erschienen in
International Journal on Software Tools for Technology Transfer / Ausgabe 2/2016
Print ISSN: 1433-2779
Elektronische ISSN: 1433-2787
DOI
https://doi.org/10.1007/s10009-015-0382-1

Weitere Artikel der Ausgabe 2/2016

International Journal on Software Tools for Technology Transfer 2/2016 Zur Ausgabe

TACAS 2014

Probabilistic verification and synthesis of the next generation airborne collision avoidance system

TACAS 2014

Many-core on-the-fly model checking of safety properties using GPUs

TACAS 2014

Some recent advances in automated analysis

TACAS 2014

Monitoring modulo theories

TACAS 2014

FDR3: a parallel refinement checker for CSP

Tacas 2014

SATMC: a SAT-based model checker for security protocols, business processes, and security APIs

Premium Partner

    Bildnachweise