Advertisement

Variable order metrics for decision diagrams in system verification

  • Elvio G. Amparore
  • Susanna DonatelliEmail author
  • Gianfranco Ciardo
Regular Paper

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 

Notes

References

  1. 1.
    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)Google Scholar
  2. 2.
    Amparore, E.G.: A new GreatSPN GUI for GSPN editing and CSL\(^\text{TA}\) model checking. In: QEST, pp. 170–173. Springer (2014)Google Scholar
  3. 3.
    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)Google Scholar
  4. 4.
    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)Google Scholar
  5. 5.
    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)Google Scholar
  6. 6.
    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)Google Scholar
  7. 7.
    Baillargeon, S., Rivest, L.P.: The construction of stratified designs in R with the package stratification. Surv. Methodol. 37(1), 53–65 (2011)Google Scholar
  8. 8.
    Berthomieu, B., Ribet, P.O., Vernadat, F.: The tool TINA. Construction of abstract state spaces for Petri nets and time Petri nets (2004)Google Scholar
  9. 9.
    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)MathSciNetCrossRefzbMATHGoogle Scholar
  10. 10.
    Bollig, B., Wegener, I.: Improving the variable ordering of OBDDs is NP-complete. IEEE Trans. Comput. 45(9), 993–1002 (1996)CrossRefzbMATHGoogle Scholar
  11. 11.
    Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. 35, 677–691 (1986)CrossRefzbMATHGoogle Scholar
  12. 12.
    Ciardo, G., Jones, R.L., Miner, A.S., Siminiceanu, R.: Logical and stochastic modeling with SMART. Perf. Eval. 63, 578–608 (2006)CrossRefGoogle Scholar
  13. 13.
    Ciardo, G., Lüttgen, G., Siminiceanu, R.: Saturation: an efficient iteration strategy for symbolic state-space generation. In: TACAS’01, pp. 328–342 (2001)Google Scholar
  14. 14.
    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)Google Scholar
  15. 15.
    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)Google Scholar
  16. 16.
    Du, K.L., Swamy, M.N.S.: Search and Optimization by Metaheuristics. Springer, Basel (2016)CrossRefzbMATHGoogle Scholar
  17. 17.
    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)Google Scholar
  18. 18.
    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)CrossRefzbMATHGoogle Scholar
  19. 19.
    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)MathSciNetCrossRefzbMATHGoogle Scholar
  20. 20.
    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)Google Scholar
  21. 21.
    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)CrossRefGoogle Scholar
  22. 22.
    Hollander, M., Wolfe, D.A.: Nonparametric Statistical Methods. Wiley, Hoboken (1999)zbMATHGoogle Scholar
  23. 23.
    Jorn Lind-Nielsen: BuDDy Manual. http://buddy.sourceforge.net/manual/main.html (2003). Accessed 12 June 2019
  24. 24.
    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)MathSciNetzbMATHGoogle Scholar
  25. 25.
    Kamp, E.: Bandwidth, profile and wavefront reduction for static variable ordering in symbolic model checking. Tech. rep., University of Twente (June, 2015)Google Scholar
  26. 26.
    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)CrossRefGoogle Scholar
  27. 27.
    King, I.P.: An automatic reordering scheme for simultaneous equations derived from network systems. J. Numer. Methods Eng. 2(4), 523–533 (1970)CrossRefGoogle Scholar
  28. 28.
    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
  29. 29.
    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)Google Scholar
  30. 30.
    Kozak, M.: Optimal stratification using random search method in agricultural surveys. Stat. Transit. 6(5), 797–806 (2004)Google Scholar
  31. 31.
    Kwiatkowska, M., Norman, G., Parker, D.: PRISM: probabilistic model checking for performance and reliability analysis. Perform. Eval. 36(4), 40–45 (2009)CrossRefGoogle Scholar
  32. 32.
    McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Norwell, MA (1993)CrossRefzbMATHGoogle Scholar
  33. 33.
    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)Google Scholar
  34. 34.
    Murata, T.: Petri nets: properties, analysis and applications. Proc. IEEE 77(4), 541–580 (1989)CrossRefGoogle Scholar
  35. 35.
    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)Google Scholar
  36. 36.
    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)Google Scholar
  37. 37.
    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)Google Scholar
  38. 38.
    Sloan, S.W.: An algorithm for profile and wavefront reduction of sparse matrices. Int. J. Numer. Methods Eng. 23(2), 239–251 (1986)MathSciNetCrossRefzbMATHGoogle Scholar
  39. 39.
    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)Google Scholar
  40. 40.
    Somenzi, F.: Efficient manipulation of decision diagrams. STTT 3(2), 171–181 (2001)zbMATHGoogle Scholar
  41. 41.
    Thierry-Mieg, Y.: Symbolic model-checking using its-tools. In: TACAS, Lecture Notes in Computer Science, vol. 9035, pp. 231–237. Springer (2015)Google Scholar
  42. 42.
    The Boost-C++ library. http://www.boost.org/. Accessed 12 June 2019
  43. 43.
    The wCorr library by Ahmad Emad and Paul Bailey. https://cran.r-project.org/web/packages/wCorr/wCorr.pdf. Accessed 12 June 2019
  44. 44.
  45. 45.
    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)CrossRefGoogle Scholar
  46. 46.
    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)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag GmbH Germany, part of Springer Nature 2019

Authors and Affiliations

  • Elvio G. Amparore
    • 1
  • Susanna Donatelli
    • 1
    Email author
  • Gianfranco Ciardo
    • 2
  1. 1.Dipartimento di InformaticaUniversità di TorinoTurinItaly
  2. 2.Computer Science DepartmentIowa State UniversityAmesUSA

Personalised recommendations