{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,4]],"date-time":"2026-07-04T05:03:07Z","timestamp":1783141387925,"version":"3.54.6"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319681665","type":"print"},{"value":"9783319681672","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-68167-2_13","type":"book-chapter","created":{"date-parts":[[2017,9,25]],"date-time":"2017-09-25T23:50:53Z","timestamp":1506383453000},"page":"184-200","source":"Crossref","is-referenced-by-count":12,"title":["Gradient-Based Variable Ordering of Decision Diagrams for Systems with Structural Units"],"prefix":"10.1007","author":[{"given":"Elvio Gilberto","family":"Amparore","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marco","family":"Beccuti","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Susanna","family":"Donatelli","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2017,9,27]]},"reference":[{"issue":"1","key":"13_CR1","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1142\/S0218126698000043","volume":"8","author":"WM Aalst Van der","year":"1998","unstructured":"Van der Aalst, W.M.: The application of Petri nets to workflow management. J. Circ. Syst. Comput. 8(1), 21\u201366 (1998)","journal-title":"J. Circ. Syst. Comput."},{"key":"13_CR2","volume-title":"Modelling with Generalized Stochastic Petri Nets","author":"M Ajmone-Marsan","year":"1995","unstructured":"Ajmone-Marsan, M., Balbo, G., Conte, G., Donatelli, S., Franceschinis, G.: Modelling with Generalized Stochastic Petri Nets. Wiley, Hoboken (1995)"},{"key":"13_CR3","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, New York (2003)","DOI":"10.1145\/764808.764839"},{"key":"13_CR4","series-title":"Springer Series in Reliability Engineering","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/978-3-319-30599-8_9","volume-title":"Principles of Performance and Reliability Modeling and Evaluation: Essays in Honor of Kishor Trivedi","author":"EG Amparore","year":"2016","unstructured":"Amparore, E.G., Balbo, G., Beccuti, M., Donatelli, S., Franceschinis, G.: 30 years of GreatSPN. In: Fiondella, L., Puliafito, A. (eds.) Principles of Performance and Reliability Modeling and Evaluation: Essays in Honor of Kishor Trivedi. SSRE, pp. 227\u2013254. Springer, Cham (2016). doi: 10.1007\/978-3-319-30599-8_9"},{"key":"13_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/978-3-319-07734-5_19","volume-title":"Application and Theory of Petri Nets and Concurrency","author":"EG Amparore","year":"2014","unstructured":"Amparore, E.G., Beccuti, M., Donatelli, S.: (Stochastic) model checking in GreatSPN. In: Ciardo, G., Kindler, E. (eds.) PETRI NETS 2014. LNCS, vol. 8489, pp. 354\u2013363. Springer, Cham (2014). doi: 10.1007\/978-3-319-07734-5_19"},{"key":"13_CR6","doi-asserted-by":"crossref","unstructured":"Amparore, E.G., Donatelli, S., Beccuti, M., Garbi, G., Miner, A.: Decision diagrams for Petri nets: which variable ordering? In: Petri Net Performance Engineering conference (PNSE), pp. 31\u201350. CEUR-WS (2017)","DOI":"10.1007\/978-3-662-58381-4_4"},{"key":"13_CR7","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, Los Alamitos, CA, USA, pp. 195\u2013196. IEEE Computer Society (2010)","DOI":"10.1109\/QEST.2010.34"},{"key":"13_CR8","doi-asserted-by":"crossref","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":"13_CR9","volume-title":"Introduction to Discrete Event Systems","author":"CG Cassandras","year":"2006","unstructured":"Cassandras, C.G., Lafortune, S.: Introduction to Discrete Event Systems. Springer, Secaucus (2006)"},{"key":"13_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/3-540-45319-9_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Ciardo","year":"2001","unstructured":"Ciardo, G., L\u00fcttgen, G., Siminiceanu, R.: Saturation: an efficient iteration strategy for symbolic state-space generation. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 328\u2013342. Springer, Heidelberg (2001). doi: 10.1007\/3-540-45319-9_23"},{"key":"13_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/978-3-540-73094-1_8","volume-title":"Petri Nets and Other Models of Concurrency \u2013 ICATPN 2007","author":"G Ciardo","year":"2007","unstructured":"Ciardo, G., L\u00fcttgen, G., Yu, A.J.: Improving static variable orders via invariants. In: Kleijn, J., Yakovlev, A. (eds.) ICATPN 2007. LNCS, vol. 4546, pp. 83\u2013103. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-73094-1_8"},{"key":"13_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/3-540-53863-1_22","volume-title":"Advances in Petri Nets 1990","author":"JM Colom","year":"1991","unstructured":"Colom, J.M., Silva, M.: Convex geometry and semiflows in P\/T nets. A comparative study of algorithms for computation of minimal p-semiflows. In: Rozenberg, G. (ed.) ICATPN 1989. LNCS, vol. 483, pp. 79\u2013112. Springer, Heidelberg (1991). doi: 10.1007\/3-540-53863-1_22"},{"key":"13_CR13","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":"13_CR14","unstructured":"Kordon, F., et al.: Complete Results for the 2016th Edition of the Model Checking Contest. http:\/\/mcc.lip.6.fr\/2016\/results.php"},{"key":"13_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/978-3-319-19488-2_9","volume-title":"Application and Theory of Petri Nets and Concurrency","author":"H Garavel","year":"2015","unstructured":"Garavel, H.: Nested-unit Petri nets: a structural means to increase efficiency and scalability of verification on elementary nets. In: Devillers, R., Valmari, A. (eds.) PETRI NETS 2015. LNCS, vol. 9115, pp. 179\u2013199. Springer, Cham (2015). doi: 10.1007\/978-3-319-19488-2_9"},{"key":"13_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"286","DOI":"10.1007\/978-3-662-53401-4_14","volume-title":"Transactions on Petri Nets and Other Models of Concurrency XI","author":"M Heiner","year":"2016","unstructured":"Heiner, M., Rohr, C., Schwarick, M., Tovchigrechko, A.A.: MARCIE\u2019s secrets of efficient model checking. In: Koutny, M., Desel, J., Kleijn, J. (eds.) Transactions on Petri Nets and Other Models of Concurrency XI. LNCS, vol. 9930, pp. 286\u2013296. Springer, Heidelberg (2016). doi: 10.1007\/978-3-662-53401-4_14"},{"issue":"4","key":"13_CR17","doi-asserted-by":"crossref","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."},{"issue":"3","key":"13_CR18","doi-asserted-by":"crossref","first-page":"559","DOI":"10.1007\/BF02510240","volume":"37","author":"G Kumfert","year":"1997","unstructured":"Kumfert, G., Pothen, A.: Two improved algorithms for envelope and wavefront reduction. BIT Numer. Math. 37(3), 559\u2013590 (1997)","journal-title":"BIT Numer. Math."},{"key":"13_CR19","doi-asserted-by":"crossref","unstructured":"Lu, Y., Jain, J., Clarke, E., Fujita, M.: Efficient variable ordering using a BDD based sampling. In: Proceedings of the 37th Annual Design Automation Conference, DAC 2000, pp. 687\u2013692. ACM, New York (2000)","DOI":"10.1145\/337292.337614"},{"key":"13_CR20","doi-asserted-by":"crossref","unstructured":"Malik, S., Wang, A.R., Brayton, R.K., Sangiovanni-Vincentelli, A.: Logic verification using binary decision diagrams in a logic synthesis environment. In: IEEE International Conference on Computer-Aided Design (ICCAD), pp. 6\u20139, November 1988","DOI":"10.1109\/ICCAD.1988.122451"},{"key":"13_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/978-3-319-40648-0_20","volume-title":"NASA Formal Methods","author":"J Meijer","year":"2016","unstructured":"Meijer, J., van de Pol, J.: Bandwidth and wavefront reduction for static variable ordering in symbolic reachability analysis. In: Rayadurgam, S., Tkachuk, O. (eds.) NFM 2016. LNCS, vol. 9690, pp. 255\u2013271. Springer, Cham (2016). doi: 10.1007\/978-3-319-40648-0_20"},{"key":"13_CR22","unstructured":"Noack, A.: A ZBDD package for efficient model checking of Petri nets (in German). Ph.D. thesis, BTU Cottbus, Department of CS (1999)"},{"key":"13_CR23","unstructured":"Rice, M., Kulhari, S.: A survey of static variable ordering heuristics for efficient BDD\/MDD construction. Technical report, University of California (2008)"},{"key":"13_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"374","DOI":"10.1007\/3-540-60029-9_50","volume-title":"Application and Theory of Petri Nets 1995","author":"O Roig","year":"1995","unstructured":"Roig, O., Cortadella, J., Pastor, E.: Verification of asynchronous circuits by BDD-based model checking of Petri nets. In: De Michelis, G., Diaz, M. (eds.) ICATPN 1995. LNCS, vol. 935, pp. 374\u2013391. Springer, Heidelberg (1995). doi: 10.1007\/3-540-60029-9_50"},{"key":"13_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1007\/3-540-36577-X_35","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K Schmidt","year":"2003","unstructured":"Schmidt, K.: Using Petri net invariants in state space construction. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 473\u2013488. Springer, Heidelberg (2003). doi: 10.1007\/3-540-36577-X_35"},{"key":"13_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1007\/11691372_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"RI Siminiceanu","year":"2006","unstructured":"Siminiceanu, R.I., Ciardo, G.: New metrics for static variable ordering in decision diagrams. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 90\u2013104. Springer, Heidelberg (2006). doi: 10.1007\/11691372_6"},{"issue":"2","key":"13_CR27","doi-asserted-by":"crossref","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. Meth. Eng. 23(2), 239\u2013251 (1986)","journal-title":"Int. J. Numer. Meth. Eng."},{"key":"13_CR28","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1046\/j.1365-2575.2000.010001001.x","volume":"10","author":"S Dongen Van","year":"2000","unstructured":"Van Dongen, S.: A cluster algorithm for graphs. Inform. Syst. 10, 1\u201340 (2000)","journal-title":"Inform. Syst."}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-68167-2_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,3]],"date-time":"2019-10-03T19:37:54Z","timestamp":1570131474000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-68167-2_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319681665","9783319681672"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-68167-2_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}