English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Tools annual

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Presents the access of premium content as premium feature

Premium Content

Global: Zendy Plus annual

Global: Zendy Free Plan

We demonstrate the applicability of bandwidth and wavefront reductionalgorithms to static variable ordering. In symbolic model checking eventlocality plays a major role in time and memory usage. For example, in Petrinets event locality can be captured by dependency matrices, where nonzeroentries indicate whether a transition modifies a place. The quality of eventlocality has been expressed as a metric called (weighted) event span. Thebandwidth of a matrix is a metric indicating the distance of nonzero elementsto the diagonal. Wavefront is a metric indicating the degree of nonzeros on oneend of the diagonal of the matrix. Bandwidth and wavefront are well studiedmetrics used in sparse matrix solvers.  In this work we prove that span is limited by twice the bandwidth of amatrix. This observation makes bandwidth reduction algorithms useful forobtaining good variable orders. One major issue we address is that thereduction algorithms can only be applied on symmetric matrices, while thedependency matrices are asymmetric. We show that the Sloan algorithm executedon the total graph of the adjacency graph gives the best variable orders.Practically, we demonstrate that our work allows to call standard sparse matrixoperations in Boost and ViennaCL, computing very good static variable orders inmilliseconds. Future work is promising, because a whole new spectrum of moreoff-the-shelf algorithms, including metaheuristic ones, become available forvariable ordering.

Bandwidth and Wavefront Reduction for Static Variable Ordering in Symbolic Model Checking