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).
Similar content being viewed by others
Notes
It could be slightly less than 10,000, since the same permutation may be randomly generated multiple times, but this is extremely unlikely except for small models.
References
Aloul, F.A., Markov, I.L., Sakallah, K.A.: FORCE: a fast and easy-to-implement variable-ordering heuristic. In: Proceedings of GLSVLSI, pp. 116–119. ACM, NY (2003)
Amparore, E.G.: A new GreatSPN GUI for GSPN editing and CSL\(^\text{TA}\) model checking. In: QEST, pp. 170–173. Springer (2014)
Amparore, E.G., Balbo, G., Beccuti, M., Donatelli, S., Franceschinis, G.: 30 years of GreatSPN, chap. In: Principles of Performance and Reliability Modeling and Evaluation: Essays in Honor of Kishor Trivedi, pp. 227–254. Springer, Cham (2016)
Amparore, E.G., Beccuti, M., Donatelli, S.: Gradient-based variable ordering of decision diagrams for systems with structural units. In: Automated Technology for Verification and Analysis, pp. 184–200. Springer (2017)
Amparore, E.G., Donatelli, S., Beccuti, M., Garbi, G., Miner, A.: Decision diagrams for Petri nets: a comparison of variable ordering algorithms. In: Transactions on Petri Nets and Other Models of Concurrency XIII pp. 73–92 (2018)
Babar, J., Miner, A.: Meddly: multi-terminal and edge-valued decision diagram library. In: International Conference on Quantitative Evaluation of Systems, pp. 195–196. IEEE Computer Society, Los Alamitos, CA, USA (2010)
Baillargeon, S., Rivest, L.P.: The construction of stratified designs in R with the package stratification. Surv. Methodol. 37(1), 53–65 (2011)
Berthomieu, B., Ribet, P.O., Vernadat, F.: The tool TINA. Construction of abstract state spaces for Petri nets and time Petri nets (2004)
Bollig, B., Löbbing, M., Wegener, I.: On the effect of local changes in the variable ordering of ordered decision diagrams. Inf. Process. Lett. 59(5), 233–239 (1996)
Bollig, B., Wegener, I.: Improving the variable ordering of OBDDs is NP-complete. IEEE Trans. Comput. 45(9), 993–1002 (1996)
Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. 35, 677–691 (1986)
Ciardo, G., Jones, R.L., Miner, A.S., Siminiceanu, R.: Logical and stochastic modeling with SMART. Perf. Eval. 63, 578–608 (2006)
Ciardo, G., Lüttgen, G., Siminiceanu, R.: Saturation: an efficient iteration strategy for symbolic state-space generation. In: TACAS’01, pp. 328–342 (2001)
Cimatti, A., Clarke, E.M., Giunchiglia, F., Roveri, M.: NUSMV: a new symbolic model verifier. In: 11th International Conference on Computer Aided Verification, pp. 495–499. Springer (1999)
Cuthill, E., McKee, J.: Reducing the bandwidth of sparse symmetric matrices. In: Proceedings of the 1969 24th National Conference, pp. 157–172. ACM, New York (1969)
Du, K.L., Swamy, M.N.S.: Search and Optimization by Metaheuristics. Springer, Basel (2016)
Fujita, M., Matsunaga, Y., Kakuda, T.: On variable ordering of binary decision diagrams for the application of multi-level logic synthesis. In: Proceedings of the Conference on European Design Automation, EURO-DAC’91, Amsterdam, The Netherlands, 1991, pp. 50–54 (1991)
Garavel, H., Lang, F., Mateescu, R., Serwe, W.: Cadp 2011: a toolbox for the construction and analysis of distributed processes. Int. J. Softw. Tools Technol. Transf. 15(2), 89–107 (2013)
Gibbs, N.E., Poole Jr., W.G., Stockmeyer, P.K.: An algorithm for reducing the bandwidth and profile of a sparse matrix. SIAM J. Numer. Anal. 13(2), 236–250 (1976)
Heiner, M., Rohr, C., Schwarick, M., Tovchigrechko, A.A.: MARCIE’s secrets of efficient model checking. In: Transactions on Petri Nets and Other Models of Concurrency XI, pp. 286–296. Springer, Heidelberg (2016)
Hocevar, D.E., Lightner, M.R., Trick, T.N.: A study of variance reduction techniques for estimating circuit yields. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 2(3), 180–192 (1983)
Hollander, M., Wolfe, D.A.: Nonparametric Statistical Methods. Wiley, Hoboken (1999)
Jorn Lind-Nielsen: BuDDy Manual. http://buddy.sourceforge.net/manual/main.html (2003). Accessed 12 June 2019
Kam, T., Villa, T., Brayton, R.K., Sangiovanni-Vincentelli, A.: Multi-valued decision diagrams: theory and applications. Mult Valued Logic 4(1), 9–62 (1992)
Kamp, E.: Bandwidth, profile and wavefront reduction for static variable ordering in symbolic model checking. Tech. rep., University of Twente (June, 2015)
Keramat, M., Kielbasa, R.: A study of stratified sampling in variance reduction techniques for parametric yield estimation. IEEE Trans. Circuits Syst. II Analog Dig. Signal Process. 45(5), 575–583 (1998)
King, I.P.: An automatic reordering scheme for simultaneous equations derived from network systems. J. Numer. Methods Eng. 2(4), 523–533 (1970)
Kordon, F., Garavel, H., Hillah, L.M., Hulin-Hubard, F., Berthomieu, B., Ciardo, G., Colange, M., Dal Zilio, S., Amparore, E., Beccuti, M., Liebke, T., Meijer, J., Miner, A., Rohr, C., Srba, J., Thierry-Mieg, Y., van de Pol, J., Wolf, K.: Complete Results for the 2017 Edition of the Model Checking Contest. http://mcc.lip6.fr/2017/results.php (2017). Accessed 12 June 2019
Kordon, F., Garavel, H., Hillah, L.M., Paviot-Adet, E., Jezequel, L., Hulin-Hubard, F., Amparore, E., Beccuti, M., Berthomieu, B., Evrard, H., Jensen, P.G., Botlan, D.L., Liebke, T., Meijer, J., Srba, J., Thierry-Mieg, Y., van de Pol, J., Wolf, K.: MCC2017—The Seventh Model Checking Contest. Accepted for publication at TopNoC, Springer (2017)
Kozak, M.: Optimal stratification using random search method in agricultural surveys. Stat. Transit. 6(5), 797–806 (2004)
Kwiatkowska, M., Norman, G., Parker, D.: PRISM: probabilistic model checking for performance and reliability analysis. Perform. Eval. 36(4), 40–45 (2009)
McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Norwell, MA (1993)
Meijer, J., van de Pol, J.: Bandwidth and wavefront reduction for static variable ordering in symbolic reachability analysis. In: NASA Formal Methods, 2016, pp. 255–271. Springer, Cham (2016)
Murata, T.: Petri nets: properties, analysis and applications. Proc. IEEE 77(4), 541–580 (1989)
Rudell, R.: Dynamic variable ordering for ordered binary decision diagrams. In: Proceedings of the 1993 IEEE/ACM International Conference on Computer-aided Design, ICCAD’93, pp. 42–47. IEEE Computer Society Press, Los Alamitos, CA, USA (1993)
Schwarick, M., Heiner, M., Rohr, C.: Marcie-model checking and reachability analysis done efficiently. In: 2011 8th International Conference on Quantitative Evaluation of Systems (QEST), pp. 91–100 (2011)
Siminiceanu, R.I., Ciardo, G.: New metrics for static variable ordering in decision diagrams. In: 12th International Conference TACAS 2006, pp. 90–104. Springer, Heidelberg (2006)
Sloan, S.W.: An algorithm for profile and wavefront reduction of sparse matrices. Int. J. Numer. Methods Eng. 23(2), 239–251 (1986)
Smith, B., Ciardo, G.: SOUPS: a variable ordering metric for the saturation algorithm. In: 18th International Conference on Application of Concurrency to System Design, ACSD 2018, Bratislava, Slovakia, June 25–29, 2018, pp. 1–10. IEEE Computer Society (2018)
Somenzi, F.: Efficient manipulation of decision diagrams. STTT 3(2), 171–181 (2001)
Thierry-Mieg, Y.: Symbolic model-checking using its-tools. In: TACAS, Lecture Notes in Computer Science, vol. 9035, pp. 231–237. Springer (2015)
The Boost-C++ library. http://www.boost.org/. Accessed 12 June 2019
The wCorr library by Ahmad Emad and Paul Bailey. https://cran.r-project.org/web/packages/wCorr/wCorr.pdf. Accessed 12 June 2019
The wCorr formulas. https://cran.r-project.org/web/packages/wCorr/vignettes/wCorrFormulas.html. Accessed 12 June 2019
van Dijk, T., Hahn, E.M., Jansen, D.N., Li, Y., Neele, T., Stoelinga, M., Turrini, A., Zhang, L.: A comparative study of BDD packages for probabilistic symbolic model checking. In: Li, X., Liu, Z., Yi, W. (eds.) Dependable Software Engineering: Theories, Tools, and Applications, pp. 35–51. Springer, Cham (2015)
van Dijk, T., van de Pol, J.: Sylvan: multi-core framework for decision diagrams. Int. J. Softw. Tools Technol. Transf. 19(6), 675–696 (2017)
Author information
Authors and Affiliations
Corresponding author
Additional information
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
This work was supported in part by the National Science Foundation under Grant ACI-1642397.
Appendix: Weighted spearman correlation
Appendix: Weighted spearman correlation
We summarize the formulas used to compute the weighted Spearman correlation coefficient from a weighted bivariate series (X, Y, W) used by the “wCorr” package [43]. A more detailed explanation can be found in [44]. The Pearson correlation coefficient \(\sigma _{P}(X,Y)\) is defined as \(\tfrac{\sigma _{X,Y}}{\sigma _X \sigma _Y}\) where \(\sigma _{X,Y}\) is the covariance between X and Y, and \(\sigma _X\) and \(\sigma _Y\) are the standard deviations of X and Y, respectively. The weighted Pearson correlation coefficient is defined as:
where \({\bar{x}}\) and \({\bar{y}}\) are the weighted means of X and Y:
using \(w_i\) as the weights. The Spearman coefficient \(\sigma _{S}(X,Y)\) is defined as the Pearson coefficient over the ranks \(X'\) and \(Y'\) of X and Y, i.e., the values of X and Y are replaced with their relative position. The weighted Spearman coefficient \(\sigma _{S}(X,Y,W)\) is computed as the weighted Pearson coefficient \(\sigma _{P}(X',Y',W)\) where \(X'\) and \(Y'\) are the weighted ranks \(X'\) and \(Y'\) of X and Y, defined so that the j-th element of X has rank
where \(n_j\) is the number of entries in X having value \(x_j\), and \({\bar{w}}_j\) is the average weight of those entries. The weighted ranks \(Y'\) of Y are defined analogously. Note that \(\sigma _{S}(X,Y,W)\) equals \(\sigma _{S}(X,Y)\) when all weights W are equal.
Rights and permissions
About this article
Cite this article
Amparore, E.G., Donatelli, S. & Ciardo, G. Variable order metrics for decision diagrams in system verification. Int J Softw Tools Technol Transfer 22, 541–562 (2020). https://doi.org/10.1007/s10009-019-00522-6
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10009-019-00522-6