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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • 5 Citations

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.
LanguageEnglish
Title of host publicationNASA Formal Methods
Subtitle of host publication8th International Symposium, NFM 2016, Minneapolis, MN, USA, June 7-9, 2016, Proceedings
EditorsSanjai Rayadurgam, Oksana Tkachuk
PublisherSpringer International Publishing
Pages255-271
Number of pages15
ISBN (Print)978-3-319-40647-3
DOIs
StatePublished - 7 Jun 2016
Event8th International Symposium on NASA Formal Methods, NFM 2016 - Minneapolis, United States
Duration: 7 Jun 20169 Jun 2016
Conference number: 8
http://crisys.cs.umn.edu/nfm2016/

Publication series

NameLecture Notes in Computer Science
PublisherSpringer International Publishing
Volume9690
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference8th International Symposium on NASA Formal Methods, NFM 2016
Abbreviated titleNFM
CountryUnited States
CityMinneapolis
Period7/06/169/06/16
Internet address

Fingerprint

Wavefronts
Bandwidth
Petri nets

Keywords

  • Wavefront
  • Sparse matrix
  • Symbolic reachability
  • Petri net
  • EWI-27067
  • IR-100721
  • Event locality
  • Event span
  • Decision diagram
  • Profile
  • METIS-318457
  • Bandwidth

Cite this

Meijer, J., & van de Pol, J. C. (2016). Bandwidth and Wavefront Reduction for Static Variable Ordering in Symbolic Reachability Analysis. In S. Rayadurgam, & O. Tkachuk (Eds.), NASA Formal Methods: 8th International Symposium, NFM 2016, Minneapolis, MN, USA, June 7-9, 2016, Proceedings (pp. 255-271). (Lecture Notes in Computer Science; Vol. 9690). Springer International Publishing. DOI: 10.1007/978-3-319-40648-0_20
Meijer, Jeroen ; van de Pol, Jan Cornelis. / Bandwidth and Wavefront Reduction for Static Variable Ordering in Symbolic Reachability Analysis. NASA Formal Methods: 8th International Symposium, NFM 2016, Minneapolis, MN, USA, June 7-9, 2016, Proceedings. editor / Sanjai Rayadurgam ; Oksana Tkachuk. Springer International Publishing, 2016. pp. 255-271 (Lecture Notes in Computer Science).
@inproceedings{a64a29305aa84daca8c9427709d8a1e3,
title = "Bandwidth and Wavefront Reduction for Static Variable Ordering in Symbolic Reachability Analysis",
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.",
keywords = "Wavefront, Sparse matrix, Symbolic reachability, Petri net, EWI-27067, IR-100721, Event locality, Event span, Decision diagram, Profile, METIS-318457, Bandwidth",
author = "Jeroen Meijer and {van de Pol}, {Jan Cornelis}",
year = "2016",
month = "6",
day = "7",
doi = "10.1007/978-3-319-40648-0_20",
language = "English",
isbn = "978-3-319-40647-3",
series = "Lecture Notes in Computer Science",
publisher = "Springer International Publishing",
pages = "255--271",
editor = "Sanjai Rayadurgam and Oksana Tkachuk",
booktitle = "NASA Formal Methods",

}

Meijer, J & van de Pol, JC 2016, Bandwidth and Wavefront Reduction for Static Variable Ordering in Symbolic Reachability Analysis. in S Rayadurgam & O Tkachuk (eds), NASA Formal Methods: 8th International Symposium, NFM 2016, Minneapolis, MN, USA, June 7-9, 2016, Proceedings. Lecture Notes in Computer Science, vol. 9690, Springer International Publishing, pp. 255-271, 8th International Symposium on NASA Formal Methods, NFM 2016, Minneapolis, United States, 7/06/16. DOI: 10.1007/978-3-319-40648-0_20

Bandwidth and Wavefront Reduction for Static Variable Ordering in Symbolic Reachability Analysis. / Meijer, Jeroen; van de Pol, Jan Cornelis.

NASA Formal Methods: 8th International Symposium, NFM 2016, Minneapolis, MN, USA, June 7-9, 2016, Proceedings. ed. / Sanjai Rayadurgam; Oksana Tkachuk. Springer International Publishing, 2016. p. 255-271 (Lecture Notes in Computer Science; Vol. 9690).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

TY - GEN

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

AU - Meijer,Jeroen

AU - van de Pol,Jan Cornelis

PY - 2016/6/7

Y1 - 2016/6/7

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

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

KW - Wavefront

KW - Sparse matrix

KW - Symbolic reachability

KW - Petri net

KW - EWI-27067

KW - IR-100721

KW - Event locality

KW - Event span

KW - Decision diagram

KW - Profile

KW - METIS-318457

KW - Bandwidth

U2 - 10.1007/978-3-319-40648-0_20

DO - 10.1007/978-3-319-40648-0_20

M3 - Conference contribution

SN - 978-3-319-40647-3

T3 - Lecture Notes in Computer Science

SP - 255

EP - 271

BT - NASA Formal Methods

PB - Springer International Publishing

ER -

Meijer J, van de Pol JC. Bandwidth and Wavefront Reduction for Static Variable Ordering in Symbolic Reachability Analysis. In Rayadurgam S, Tkachuk O, editors, NASA Formal Methods: 8th International Symposium, NFM 2016, Minneapolis, MN, USA, June 7-9, 2016, Proceedings. Springer International Publishing. 2016. p. 255-271. (Lecture Notes in Computer Science). Available from, DOI: 10.1007/978-3-319-40648-0_20