{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T06:25:47Z","timestamp":1745994347338},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662583807"},{"type":"electronic","value":"9783662583814"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-662-58381-4_4","type":"book-chapter","created":{"date-parts":[[2018,11,20]],"date-time":"2018-11-20T09:48:09Z","timestamp":1542707289000},"page":"73-92","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Decision Diagrams for Petri Nets: A Comparison of Variable Ordering Algorithms"],"prefix":"10.1007","author":[{"given":"Elvio Gilberto","family":"Amparore","sequence":"first","affiliation":[]},{"given":"Susanna","family":"Donatelli","sequence":"additional","affiliation":[]},{"given":"Marco","family":"Beccuti","sequence":"additional","affiliation":[]},{"given":"Giulio","family":"Garbi","sequence":"additional","affiliation":[]},{"given":"Andrew","family":"Miner","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,11,21]]},"reference":[{"key":"4_CR1","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1145\/190.191","volume":"2","author":"M Ajmone Marsan","year":"1984","unstructured":"Ajmone Marsan, M., Conte, G., Balbo, G.: A class of generalized stochastic Petri nets for the performance evaluation of multiprocessor systems. ACM Trans. Comput. Syst. 2, 93\u2013122 (1984)","journal-title":"ACM Trans. Comput. Syst."},{"key":"4_CR2","unstructured":"Aldinucci, M., Bagnasco, S., Lusso, S., Pasteris, P., Vallero, S., Rabellino, S.: The open computing cluster for advanced data manipulation (OCCAM). In: 22nd International Conference on Computing in High Energy and Nuclear Physics, San Francisco (2016)"},{"key":"4_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":"4_CR4","unstructured":"Amparore, E.G.: Reengineering the editor of the GreatSPN framework. In: PNSE@ Petri Nets, pp. 153\u2013170 (2015)"},{"key":"4_CR5","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","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. SSRE, pp. 227\u2013254. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-30599-8_9"},{"key":"4_CR6","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). https:\/\/doi.org\/10.1007\/978-3-319-07734-5_19"},{"key":"4_CR7","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":"4_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-319-68167-2_13","volume-title":"Automated Technology for Verification and Analysis","author":"EG Amparore","year":"2017","unstructured":"Amparore, E.G., Beccuti, M., Donatelli, S.: Gradient-based variable ordering of decision diagrams for systems with structural units. In: D\u2019Souza, D., Narayan Kumar, K. (eds.) ATVA 2017. LNCS, vol. 10482, pp. 184\u2013200. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-68167-2_13"},{"issue":"4","key":"4_CR9","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1145\/1530873.1530876","volume":"36","author":"S Baarir","year":"2009","unstructured":"Baarir, S., Beccuti, M., Cerotti, D., Pierro, M.D., Donatelli, S., Franceschinis, G.: The GreatSPN tool: recent enhancements. Perform. Eval. 36(4), 4\u20139 (2009)","journal-title":"Perform. Eval."},{"key":"4_CR10","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 (2010)","DOI":"10.1109\/QEST.2010.34"},{"issue":"9","key":"4_CR11","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":"4_CR12","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":"4_CR13","unstructured":"Burch, J.R., Clarke, E.M., Long, D.E.: Symbolic model checking with partitioned transition relations. In: IFIP TC10\/WG 10.5 Very Large Scale Integration, pp. 49\u201358. North-Holland (1991)"},{"key":"4_CR14","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\u2014space generation. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 328\u2013342. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45319-9_23"},{"key":"4_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/3-540-36577-X_27","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Ciardo","year":"2003","unstructured":"Ciardo, G., Marmorstein, R., Siminiceanu, R.: Saturation unbound. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 379\u2013393. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-36577-X_27"},{"key":"4_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/11560548_13","volume-title":"Correct Hardware Design and Verification Methods","author":"G Ciardo","year":"2005","unstructured":"Ciardo, G., Yu, A.J.: Saturation-based symbolic reachability analysis using conjunctive and disjunctive partitioning. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 146\u2013161. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11560548_13"},{"key":"4_CR17","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":"4_CR18","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). https:\/\/doi.org\/10.1007\/978-3-319-19488-2_9"},{"issue":"2","key":"4_CR19","first-page":"236","volume":"13","author":"N Gibbs","year":"1976","unstructured":"Gibbs, N., Poole, W., Stockmeyer, P.: An algorithm for reducing the bandwidth and profile of a sparse matrix. SIAM J. 13(2), 236\u2013250 (1976)","journal-title":"SIAM J."},{"key":"4_CR20","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). https:\/\/doi.org\/10.1007\/978-3-662-53401-4_14"},{"key":"4_CR21","unstructured":"Kamp, E.: Bandwidth, profile and wavefront reduction for static variable ordering in symbolic model checking. University of Twente, Technical report, June 2015"},{"issue":"4","key":"4_CR22","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":"4_CR23","unstructured":"Kordon, F., et al.: Complete Results for the 2017 Edition of the Model Checking Contest, June 2017. http:\/\/mcc.lip6.fr\/2017\/results.php"},{"issue":"3","key":"4_CR24","doi-asserted-by":"publisher","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":"4_CR25","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). https:\/\/doi.org\/10.1007\/978-3-319-40648-0_20"},{"issue":"1\u20134","key":"4_CR26","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1016\/j.peva.2003.07.005","volume":"56","author":"AS Miner","year":"2004","unstructured":"Miner, A.S.: Implicit GSPN reachability set generation using decision diagrams. Perform. Eval. 56(1\u20134), 145\u2013165 (2004)","journal-title":"Perform. Eval."},{"key":"4_CR27","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":"4_CR28","unstructured":"Rice, M., Kulhari, S.: A survey of static variable ordering heuristics for efficient BDD\/MDD construction. University of California, Technical report (2008)"},{"issue":"2","key":"4_CR29","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":"4_CR30","unstructured":"Tovchigrechko, A.: Model checking using interval decision diagrams. Ph.D. thesis, BTU Cottbus, Department of CS (2008)"},{"key":"4_CR31","doi-asserted-by":"publisher","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","Transactions on Petri Nets and Other Models of Concurrency XIII"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-58381-4_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,11,5]],"date-time":"2019-11-05T14:41:41Z","timestamp":1572964901000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-58381-4_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783662583807","9783662583814"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-58381-4_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}