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

Jeroen Meijer; Jan Cornelis van de Pol

doi:10.1007/978-3-319-40648-0_20

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

Jeroen Meijer, Jan Cornelis van de Pol

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

20 Citations (Scopus)

549 Downloads (Pure)

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.

Original language	English
Title of host publication	NASA Formal Methods
Subtitle of host publication	8th International Symposium, NFM 2016, Minneapolis, MN, USA, June 7-9, 2016, Proceedings
Editors	Sanjai Rayadurgam, Oksana Tkachuk
Publisher	Springer
Pages	255-271
Number of pages	15
ISBN (Print)	978-3-319-40647-3
DOIs	https://doi.org/10.1007/978-3-319-40648-0_20
Publication status	Published - 7 Jun 2016
Event	8th International Symposium on NASA Formal Methods, NFM 2016 - Minneapolis, United States Duration: 7 Jun 2016 → 9 Jun 2016 Conference number: 8 http://crisys.cs.umn.edu/nfm2016/

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer International Publishing
Volume	9690
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	8th International Symposium on NASA Formal Methods, NFM 2016
Abbreviated title	NFM
Country/Territory	United States
City	Minneapolis
Period	7/06/16 → 9/06/16
Internet address	http://crisys.cs.umn.edu/nfm2016/

Keywords

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

Access to Document

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

main(3)Accepted author version, 469 KB
powerpoint presentatonFinal published version, 875 KB

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. https://doi.org/10.1007/978-3-319-40648-0_20

@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{\textquoteright}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 = jun,

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",

pages = "255--271",

editor = "Sanjai Rayadurgam and Oksana Tkachuk",

booktitle = "NASA Formal Methods",

address = "Germany",

note = "8th International Symposium on NASA Formal Methods, NFM 2016, NFM ; Conference date: 07-06-2016 Through 09-06-2016",

url = "http://crisys.cs.umn.edu/nfm2016/",

}

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, pp. 255-271, 8th International Symposium on NASA Formal Methods, NFM 2016, Minneapolis, Minnesota, United States, 7/06/16. https://doi.org/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, 2016. p. 255-271 (Lecture Notes in Computer Science; Vol. 9690).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

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

AU - Meijer, Jeroen

AU - van de Pol, Jan Cornelis

N1 - Conference code: 8

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

A2 - Rayadurgam, Sanjai

A2 - Tkachuk, Oksana

PB - Springer

T2 - 8th International Symposium on NASA Formal Methods, NFM 2016

Y2 - 7 June 2016 through 9 June 2016

ER -

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

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this