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

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    15 Citations (Scopus)
    124 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 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
    Pages255-271
    Number of pages15
    ISBN (Print)978-3-319-40647-3
    DOIs
    Publication statusPublished - 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

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