{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,29]],"date-time":"2026-09-29T10:08:25Z","timestamp":1790676505138,"version":"4.1.0"},"reference-count":46,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2019,6,14]],"date-time":"2019-06-14T00:00:00Z","timestamp":1560470400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2019,6,14]],"date-time":"2019-06-14T00:00:00Z","timestamp":1560470400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2020,10]]},"DOI":"10.1007\/s10009-019-00522-6","type":"journal-article","created":{"date-parts":[[2019,6,14]],"date-time":"2019-06-14T19:02:36Z","timestamp":1560538956000},"page":"541-562","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Variable order metrics for decision diagrams in system verification"],"prefix":"10.1007","volume":"22","author":[{"given":"Elvio G.","family":"Amparore","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Susanna","family":"Donatelli","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Gianfranco","family":"Ciardo","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2019,6,14]]},"reference":[{"key":"522_CR1","doi-asserted-by":"crossref","unstructured":"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\u2013119. ACM, NY (2003)","DOI":"10.1145\/764808.764839"},{"key":"522_CR2","doi-asserted-by":"crossref","unstructured":"Amparore, E.G.: A new GreatSPN GUI for GSPN editing and CSL$$^\\text{TA}$$ model checking. In: QEST, pp. 170\u2013173. Springer (2014)","DOI":"10.1007\/978-3-319-10696-0_13"},{"key":"522_CR3","doi-asserted-by":"crossref","unstructured":"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\u2013254. Springer, Cham (2016)","DOI":"10.1007\/978-3-319-30599-8_9"},{"key":"522_CR4","doi-asserted-by":"crossref","unstructured":"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\u2013200. Springer (2017)","DOI":"10.1007\/978-3-319-68167-2_13"},{"key":"522_CR5","doi-asserted-by":"crossref","unstructured":"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\u201392 (2018)","DOI":"10.1007\/978-3-662-58381-4_4"},{"key":"522_CR6","doi-asserted-by":"crossref","unstructured":"Babar, J., Miner, A.: Meddly: multi-terminal and edge-valued decision diagram library. In: International Conference on Quantitative Evaluation of Systems, pp. 195\u2013196. IEEE Computer Society, Los Alamitos, CA, USA (2010)","DOI":"10.1109\/QEST.2010.34"},{"issue":"1","key":"522_CR7","first-page":"53","volume":"37","author":"S Baillargeon","year":"2011","unstructured":"Baillargeon, S., Rivest, L.P.: The construction of stratified designs in R with the package stratification. Surv. Methodol. 37(1), 53\u201365 (2011)","journal-title":"Surv. Methodol."},{"key":"522_CR8","doi-asserted-by":"crossref","unstructured":"Berthomieu, B., Ribet, P.O., Vernadat, F.: The tool TINA. Construction of abstract state spaces for Petri nets and time Petri nets (2004)","DOI":"10.1080\/00207540412331312688"},{"issue":"5","key":"522_CR9","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1016\/0020-0190(96)00119-6","volume":"59","author":"B Bollig","year":"1996","unstructured":"Bollig, B., L\u00f6bbing, M., Wegener, I.: On the effect of local changes in the variable ordering of ordered decision diagrams. Inf. Process. Lett. 59(5), 233\u2013239 (1996)","journal-title":"Inf. Process. Lett."},{"issue":"9","key":"522_CR10","doi-asserted-by":"publisher","first-page":"993","DOI":"10.1109\/12.537122","volume":"45","author":"B Bollig","year":"1996","unstructured":"Bollig, B., Wegener, I.: Improving the variable ordering of OBDDs is NP-complete. IEEE Trans. Comput. 45(9), 993\u20131002 (1996)","journal-title":"IEEE Trans. Comput."},{"key":"522_CR11","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"RE Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. 35, 677\u2013691 (1986)","journal-title":"IEEE Trans. Comput."},{"key":"522_CR12","doi-asserted-by":"publisher","first-page":"578","DOI":"10.1016\/j.peva.2005.06.001","volume":"63","author":"G Ciardo","year":"2006","unstructured":"Ciardo, G., Jones, R.L., Miner, A.S., Siminiceanu, R.: Logical and stochastic modeling with SMART. Perf. Eval. 63, 578\u2013608 (2006)","journal-title":"Perf. Eval."},{"key":"522_CR13","doi-asserted-by":"crossref","unstructured":"Ciardo, G., L\u00fcttgen, G., Siminiceanu, R.: Saturation: an efficient iteration strategy for symbolic state-space generation. In: TACAS\u201901, pp. 328\u2013342 (2001)","DOI":"10.1007\/3-540-45319-9_23"},{"key":"522_CR14","doi-asserted-by":"crossref","unstructured":"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\u2013499. Springer (1999)","DOI":"10.1007\/3-540-48683-6_44"},{"key":"522_CR15","doi-asserted-by":"crossref","unstructured":"Cuthill, E., McKee, J.: Reducing the bandwidth of sparse symmetric matrices. In: Proceedings of the 1969 24th National Conference, pp. 157\u2013172. ACM, New York (1969)","DOI":"10.1145\/800195.805928"},{"key":"522_CR16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41192-7","volume-title":"Search and Optimization by Metaheuristics","author":"KL Du","year":"2016","unstructured":"Du, K.L., Swamy, M.N.S.: Search and Optimization by Metaheuristics. Springer, Basel (2016)"},{"key":"522_CR17","unstructured":"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\u201991, Amsterdam, The Netherlands, 1991, pp. 50\u201354 (1991)"},{"issue":"2","key":"522_CR18","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/s10009-012-0244-z","volume":"15","author":"H Garavel","year":"2013","unstructured":"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\u2013107 (2013)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"2","key":"522_CR19","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1137\/0713023","volume":"13","author":"NE Gibbs","year":"1976","unstructured":"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\u2013250 (1976)","journal-title":"SIAM J. Numer. Anal."},{"key":"522_CR20","doi-asserted-by":"crossref","unstructured":"Heiner, M., Rohr, C., Schwarick, M., Tovchigrechko, A.A.: MARCIE\u2019s secrets of efficient model checking. In: Transactions on Petri Nets and Other Models of Concurrency XI, pp. 286\u2013296. Springer, Heidelberg (2016)","DOI":"10.1007\/978-3-662-53401-4_14"},{"issue":"3","key":"522_CR21","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1109\/TCAD.1983.1270035","volume":"2","author":"DE Hocevar","year":"1983","unstructured":"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\u2013192 (1983)","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"522_CR22","volume-title":"Nonparametric Statistical Methods","author":"M Hollander","year":"1999","unstructured":"Hollander, M., Wolfe, D.A.: Nonparametric Statistical Methods. Wiley, Hoboken (1999)"},{"key":"522_CR23","unstructured":"Jorn Lind-Nielsen: BuDDy Manual. \nhttp:\/\/buddy.sourceforge.net\/manual\/main.html\n\n (2003). Accessed 12 June 2019"},{"issue":"1","key":"522_CR24","first-page":"9","volume":"4","author":"T Kam","year":"1992","unstructured":"Kam, T., Villa, T., Brayton, R.K., Sangiovanni-Vincentelli, A.: Multi-valued decision diagrams: theory and applications. Mult Valued Logic 4(1), 9\u201362 (1992)","journal-title":"Mult Valued Logic"},{"key":"522_CR25","unstructured":"Kamp, E.: Bandwidth, profile and wavefront reduction for static variable ordering in symbolic model checking. Tech. rep., University of Twente (June, 2015)"},{"issue":"5","key":"522_CR26","doi-asserted-by":"publisher","first-page":"575","DOI":"10.1109\/82.673639","volume":"45","author":"M Keramat","year":"1998","unstructured":"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\u2013583 (1998)","journal-title":"IEEE Trans. Circuits Syst. II Analog Dig. Signal Process."},{"issue":"4","key":"522_CR27","doi-asserted-by":"publisher","first-page":"523","DOI":"10.1002\/nme.1620020406","volume":"2","author":"IP King","year":"1970","unstructured":"King, I.P.: An automatic reordering scheme for simultaneous equations derived from network systems. J. Numer. Methods Eng. 2(4), 523\u2013533 (1970)","journal-title":"J. Numer. Methods Eng."},{"key":"522_CR28","doi-asserted-by":"crossref","unstructured":"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\u00a0de Pol, J., Wolf, K.: Complete Results for the 2017 Edition of the Model Checking Contest. \nhttp:\/\/mcc.lip6.fr\/2017\/results.php\n\n (2017). Accessed 12 June 2019","DOI":"10.1007\/978-3-662-58381-4_9"},{"key":"522_CR29","doi-asserted-by":"crossref","unstructured":"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\u00a0de Pol, J., Wolf, K.: MCC2017\u2014The Seventh Model Checking Contest. Accepted for publication at TopNoC, Springer (2017)","DOI":"10.1007\/978-3-662-58381-4_9"},{"issue":"5","key":"522_CR30","first-page":"797","volume":"6","author":"M Kozak","year":"2004","unstructured":"Kozak, M.: Optimal stratification using random search method in agricultural surveys. Stat. Transit. 6(5), 797\u2013806 (2004)","journal-title":"Stat. Transit."},{"issue":"4","key":"522_CR31","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1145\/1530873.1530882","volume":"36","author":"M Kwiatkowska","year":"2009","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM: probabilistic model checking for performance and reliability analysis. Perform. Eval. 36(4), 40\u201345 (2009)","journal-title":"Perform. Eval."},{"key":"522_CR32","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"KL McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Norwell, MA (1993)"},{"key":"522_CR33","unstructured":"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\u2013271. Springer, Cham (2016)"},{"issue":"4","key":"522_CR34","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1109\/5.24143","volume":"77","author":"T Murata","year":"1989","unstructured":"Murata, T.: Petri nets: properties, analysis and applications. Proc. IEEE 77(4), 541\u2013580 (1989)","journal-title":"Proc. IEEE"},{"key":"522_CR35","unstructured":"Rudell, R.: Dynamic variable ordering for ordered binary decision diagrams. In: Proceedings of the 1993 IEEE\/ACM International Conference on Computer-aided Design, ICCAD\u201993, pp. 42\u201347. IEEE Computer Society Press, Los Alamitos, CA, USA (1993)"},{"key":"522_CR36","doi-asserted-by":"crossref","unstructured":"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\u2013100 (2011)","DOI":"10.1109\/QEST.2011.19"},{"key":"522_CR37","doi-asserted-by":"crossref","unstructured":"Siminiceanu, R.I., Ciardo, G.: New metrics for static variable ordering in decision diagrams. In: 12th International Conference TACAS 2006, pp. 90\u2013104. Springer, Heidelberg (2006)","DOI":"10.1007\/11691372_6"},{"issue":"2","key":"522_CR38","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1002\/nme.1620230208","volume":"23","author":"SW Sloan","year":"1986","unstructured":"Sloan, S.W.: An algorithm for profile and wavefront reduction of sparse matrices. Int. J. Numer. Methods Eng. 23(2), 239\u2013251 (1986)","journal-title":"Int. J. Numer. Methods Eng."},{"key":"522_CR39","unstructured":"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\u201329, 2018, pp. 1\u201310. IEEE Computer Society (2018)"},{"issue":"2","key":"522_CR40","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/s100090100042","volume":"3","author":"F Somenzi","year":"2001","unstructured":"Somenzi, F.: Efficient manipulation of decision diagrams. STTT 3(2), 171\u2013181 (2001)","journal-title":"STTT"},{"key":"522_CR41","doi-asserted-by":"crossref","unstructured":"Thierry-Mieg, Y.: Symbolic model-checking using its-tools. In: TACAS, Lecture Notes in Computer Science, vol. 9035, pp. 231\u2013237. Springer (2015)","DOI":"10.1007\/978-3-662-46681-0_20"},{"key":"522_CR42","unstructured":"The Boost-C++ library. \nhttp:\/\/www.boost.org\/\n\n. Accessed 12 June 2019"},{"key":"522_CR43","unstructured":"The wCorr library by Ahmad Emad and Paul Bailey. \nhttps:\/\/cran.r-project.org\/web\/packages\/wCorr\/wCorr.pdf\n\n. Accessed 12 June 2019"},{"key":"522_CR44","unstructured":"The wCorr formulas. \nhttps:\/\/cran.r-project.org\/web\/packages\/wCorr\/vignettes\/wCorrFormulas.html\n\n. Accessed 12 June 2019"},{"key":"522_CR45","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-319-25942-0_3","volume-title":"Dependable Software Engineering: Theories, Tools, and Applications","author":"T van Dijk","year":"2015","unstructured":"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\u201351. Springer, Cham (2015)"},{"issue":"6","key":"522_CR46","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1007\/s10009-016-0433-2","volume":"19","author":"T van Dijk","year":"2017","unstructured":"van Dijk, T., van de Pol, J.: Sylvan: multi-core framework for decision diagrams. Int. J. Softw. Tools Technol. Transf. 19(6), 675\u2013696 (2017)","journal-title":"Int. J. Softw. Tools Technol. Transf."}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-019-00522-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-019-00522-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-019-00522-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,9,28]],"date-time":"2020-09-28T07:09:05Z","timestamp":1601276945000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-019-00522-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,6,14]]},"references-count":46,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2020,10]]}},"alternative-id":["522"],"URL":"https:\/\/doi.org\/10.1007\/s10009-019-00522-6","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,6,14]]},"assertion":[{"value":"14 June 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}