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:
Temporal Logic Framework for Performance Analysis of Architectures of Systems Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

Bandwidth and Wavefront Reduction for Static Variable Ordering in Symbolic Reachability Analysis

verfasst von : Jeroen Meijer, Jaco van de Pol

Erschienen in: NASA Formal Methods

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

We investigate the use of bandwidth and wavefront reduction algorithms to determine a static BDD variable ordering. The aim is to reduce the size of BDDs arising in symbolic reachability. Previous work showed that minimizing the (weighted) event span of the variable dependency graph yields small BDDs. The bandwidth and wavefront of symmetric matrices are well studied metrics, used in sparse matrix solvers, and many bandwidth and wavefront reduction algorithms are readily available in libraries like Boost and ViennaCL.
In this paper, we transform the dependency matrix to a symmetric matrix and apply various bandwidth and wavefront reduction algorithms, measuring their influence on the (weighted) event span. We show that Sloan’s algorithm, executed on the total graph of the dependency matrix, yields a variable order with minimal event span. We demonstrate this on a large benchmark of Petri nets, Dve, Promela, B, and mcrl2 models. As a result, good static variable orders can now be determined in milliseconds by using standard sparse matrix solvers.

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 Verifying Relative Safety, Accuracy, and Termination for Program Approximations
Nächstes Kapitel Gray-Box Learning of Serial Compositions of Mealy Machines
Fußnoten
1
We restrict ourselves to languages that induce a disjunctive transition relation.
 
2
Theorem 1 can be easily proven with the triangle inequality theorem.
 
4
There are three side notes. First, \(\mu \) and \(\sigma \) for bandwidth, profile and wavefront are computed per graph type, because the bipartite and total graph have different sizes. Second, Noack1 and Noack2 can only be computed directly on Petri nets (PNML, Fig. 9e), so bandwidth, profile and wavefront are unknown. Third, when FORCE is executed or without reordering, bandwidth, profile and wavefront are not reported. The reason is that our symmetrization approach typically produces high values for those metrics. Event span does not have this problem.
 
Literatur
1.
Aloul, F.A., Markov, I.L., Sakallah, K.A.: FORCE: a fast and easy-to-implement variable-ordering heuristic. In: 13th ACM, VLSI, pp. 116–119. ACM (2003)
2.
Blom, S., van de Pol, J.: Symbolic reachability for process algebras with recursive data types. In: Fitzgerald, J.S., Haxthausen, A.E., Yenigun, H. (eds.) ICTAC 2008. LNCS, vol. 5160, pp. 81–95. Springer, Heidelberg (2008)CrossRef
3.
Bollig, B., Wegener, I.: Improving the variable ordering of OBDDs is NP-complete. IEEE Trans. Comput. 45(9), 993–1002 (1996)CrossRefMATH
4.
Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. 35(8), 677–691 (1986)CrossRefMATH
5.
Burch, J.R., Clarke, E.M., Long, D.E.: Symbolic model checking with partitioned transition relations. In: VLSI 1991 (1991)
6.
Ciardo, G., Marmorstein, R.M., Siminiceanu, R.: The saturation algorithm for symbolic state-space exploration. STTT 8(1), 4–25 (2006)CrossRef
7.
Ciardo, G., Miner, A.S., Wan, M.: Advanced features in SMART: the stochastic model checking analyzer for reliability and timing. SIGMETRICS PER 36(4), 58–63 (2009)CrossRef
8.
Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: an opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 359. Springer, Heidelberg (2002)CrossRef
9.
Cranen, S., Groote, J.F., Keiren, J.J.A., Stappers, F.P.M., de Vink, E.P., Wesselink, W., Willemse, T.A.C.: An overview of the mCRL2 toolset and its recent advances. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 199–213. Springer, Heidelberg (2013)CrossRef
10.
Cuthill, E., McKee, J.: Reducing the bandwidth of sparse symmetric matrices. In: Proceedings 24th National Conference, pp. 157–172. ACM (1969)
11.
Gibbs, N.E., Poole Jr., W.G., Stockmeyer, P.K.: An algorithm for reducing the bandwidth and profile of a sparse matrix. SIAM J. Num. Anal. 13(2), 236–250 (1976)MathSciNetCrossRefMATH
12.
Grumberg, O., Livne, S., Markovitch, S.: Learning to order BDD variables in verification. JAIR 18, 83–116 (2003)MathSciNetMATH
13.
Heiner, M., Rohr, C., Schwarick, M.: MARCIE – model checking and reachability analysis done efficiently. In: Colom, J.-M., Desel, J. (eds.) PETRI NETS 2013. LNCS, vol. 7927, pp. 389–399. Springer, Heidelberg (2013)CrossRef
14.
Kant, G., Laarman, A., Meijer, J., van de Pol, J., Blom, S., van Dijk, T.: LTSmin: high-performance language-independent model checking. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 692–707. Springer, Heidelberg (2015)
15.
Karantasis, K.I., et al.: Parallelization of reordering algorithms for bandwidth and wavefront reduction. In: ICHPC 2014, pp. 921–932. IEEE (2014)
16.
Kaveh, A.: Ordering for Optimal Patterns of Structural Matrices. Wiley, New York (2006). pp. 191–271
17.
King, I.P.: An automatic reordering scheme for simultaneous equations derived from network systems. Int. J. Numer. Meth. Eng. 2(4), 523–533 (1970)CrossRef
18.
19.
Leuschel, M., Butler, M.J.: ProB: an automated analysis toolset for the B method. STTT 10(2), 185–203 (2008)CrossRef
20.
Mafteiu-Scai, L.O.: The bandwidths of a matrix. A survey of algorithms. Ann. West Univ. Timisoara-Math. 52(2), 183–223 (2014)MathSciNet
21.
Meijer, J., Kant, G., Blom, S., van de Pol, J.: Read, write and copy dependencies for symbolic model checking. In: Yahav, E. (ed.) HVC 2014. LNCS, vol. 8855, pp. 204–219. Springer, Heidelberg (2014)
22.
Noack, A.: A ZBDD package for efficient model checking of Petri nets. Forschungsbericht, Branderburgische Technische Uinversität Cottbus (1999)
23.
Pelánek, R.: BEEM: benchmarks for explicit model checkers. In: Bošnački, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 263–267. Springer, Heidelberg (2007)CrossRef
24.
Reid, J.K., Scott, J.A.: Reducing the total bandwidth of a sparse unsymmetric matrix. SIAM J. Matrix Anal. Appl. 28(3), 805–821 (2006)MathSciNetCrossRefMATH
25.
Rice, M., Kulhari, S.: A survey of static variable ordering heuristics for efficient BDD/MDD construction. Technical report, University of California (2008)
26.
Rudell, R.: Dynamic variable ordering for ordered binary decision diagrams. In: ICCAD1993. IEEE (1993)
27.
Rupp, K., Rudolf, F., Weinbub, J.: ViennaCL - a high level linear algebra library for GPUs and multi-core CPUs. In: GPUScA 2010, pp. 51–56 (2010)
28.
Siminiceanu, R.I., Ciardo, G.: New metrics for static variable ordering in decision diagrams. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 90–104. Springer, Heidelberg (2006)CrossRef
29.
Sloan, S.W.: A FORTRAN program for profile and wavefront reduction. Int. J. Numer. Meth. Eng. 28(11), 2651–2679 (1989)CrossRefMATH
30.
Thierry-Mieg, Y.: Symbolic model-checking using ITS-tools. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 231–237. Springer, Heidelberg (2015)
Metadaten
Titel
Bandwidth and Wavefront Reduction for Static Variable Ordering in Symbolic Reachability Analysis
verfasst von
Jeroen Meijer
Jaco van de Pol
Copyright-Jahr
2016
Buch
NASA Formal Methods

Print ISBN: 978-3-319-40647-3

Electronic ISBN: 978-3-319-40648-0

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-319-40648-0_20