Variable order metrics for decision diagrams in system verification
- PDF / 2,833,830 Bytes
- 22 Pages / 595.276 x 790.866 pts Page_size
- 47 Downloads / 201 Views
REGULAR PAPER
Variable order metrics for decision diagrams in system verification Elvio G. Amparore1 · Susanna Donatelli1 · Gianfranco Ciardo2
© Springer-Verlag GmbH Germany, part of Springer Nature 2019
Abstract Decision diagrams (DDs) are widely used in system verification to compute and store the state space of finite discrete events dynamic systems (DEDSs). DDs are organized into levels, and it is well known that the size of a DD encoding a given set may be very sensitive to the order in which the variables capturing the state of the system are mapped to levels. Computing optimal orders is NP-hard. Several heuristics for variable order computation have been proposed, and metrics have been introduced to evaluate these orders. However, we know of no published evaluation that compares the actual predictive power for all these metrics. We propose and apply a methodology to carry out such an evaluation, based on the correlation between the metric value of a variable order and the size of the DD generated with that order. We compute correlations for several metrics from the literature, applied to many variable orders built using different approaches, for 40 DEDSs taken from the literature. Our experiments show that these metrics have correlations ranging from “very weak or nonexisting” to “strong.” We show the importance of highly correlating metrics on variable order heuristics, by defining and evaluating two new heuristics (an improvement of the well-known Force heuristic and a metric-based simulated annealing), as well as a meta-heuristic (that uses a metric to select the “best” variable order among a set of different variable orders). Keywords Decision diagrams · Variable order metric · Variable order computation
1 Introduction Decision diagrams (DDs), which include binary and multivalued decision diagrams (BDDs [11] and MDDs [24]), are a powerful data structure to store large structured data and are used in many system verification tools [3,12,14,31,32] to store the state space and the transition system of the discretestate system under study. It is well known [11] that the size of the DD encoding the state space of a system can be exponentially affected by the order in which state variables are mapped to DD levels, and this exponential factor is often This work was supported in part by the National Science Foundation under Grant ACI-1642397.
B
Susanna Donatelli [email protected] Elvio G. Amparore [email protected] Gianfranco Ciardo [email protected]
1
Dipartimento di Informatica, Università di Torino, Turin, Italy
2
Computer Science Department, Iowa State University, Ames, IA, USA
encountered in practical applications: indeed the user manual of the widely used NuSMV tool [14, page 103] states “In particular, the order of variables is critical to control the memory and the time required by operations over BDDs.” Unfortunately, finding an optimal order (yielding a minimal BDD for a given function) is an NP-complete problem [10]. Two standard approaches to mitigate the DD growth are to perform a dyna
Data Loading...
