{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:30:26Z","timestamp":1742913026171,"version":"3.40.3"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030174644"},{"type":"electronic","value":"9783030174651"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"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":[[2019]]},"DOI":"10.1007\/978-3-030-17465-1_16","type":"book-chapter","created":{"date-parts":[[2019,4,4]],"date-time":"2019-04-04T02:50:37Z","timestamp":1554346237000},"page":"285-302","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["i $$_\\mathrm {Rank}$$ : A Variable Order Metric for DEDS Subject to Linear Invariants"],"prefix":"10.1007","author":[{"given":"Elvio Gilberto","family":"Amparore","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gianfranco","family":"Ciardo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Susanna","family":"Donatelli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrew","family":"Miner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,4,3]]},"reference":[{"unstructured":"The GreatSPN tool homepage. http:\/\/www.di.unito.it\/~greatspn\/index.html","key":"16_CR1"},{"unstructured":"MCC: The Model Checking Competition. https:\/\/mcc.lip6.fr","key":"16_CR2"},{"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)","key":"16_CR3","DOI":"10.1145\/764808.764839"},{"key":"16_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","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":"16_CR5","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"},{"doi-asserted-by":"crossref","unstructured":"Amparore, E.G., Ciardo, G., Donatelli, S.: Variable order metrics for decision diagrams in system verification (2018, submitted for publication). http:\/\/www.di.unito.it\/~amparore\/metrics_STTT.pdf","key":"16_CR6","DOI":"10.1007\/s10009-019-00522-6"},{"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: Transactions on Petri Nets and Other Models of Concurrency XI. Springer, Heidelberg (2019, to appear)","key":"16_CR7","DOI":"10.1007\/978-3-662-58381-4_4"},{"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)","key":"16_CR8","DOI":"10.1109\/QEST.2010.34"},{"issue":"9","key":"16_CR9","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."},{"issue":"8","key":"16_CR10","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(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. Comput."},{"key":"16_CR11","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":"16_CR12","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). https:\/\/doi.org\/10.1007\/978-3-540-73094-1_8"},{"key":"16_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-3-642-29072-5_3","volume-title":"Transactions on Petri Nets and Other Models of Concurrency V","author":"G Ciardo","year":"2012","unstructured":"Ciardo, G., Zhao, Y., Jin, X.: Ten years of saturation: a Petri net perspective. In: Jensen, K., Donatelli, S., Kleijn, J. (eds.) Transactions on Petri Nets and Other Models of Concurrency V. LNCS, vol. 6900, pp. 51\u201395. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-29072-5_3"},{"key":"16_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/3-540-48683-6_44","volume-title":"Computer Aided Verification","author":"A Cimatti","year":"1999","unstructured":"Cimatti, A., Clarke, E.M., Giunchiglia, F., Roveri, M.: NuSMV: a new symbolic model verifier. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol. 1633, pp. 495\u2013499. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48683-6_44"},{"key":"16_CR15","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). https:\/\/doi.org\/10.1007\/3-540-53863-1_22"},{"key":"16_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/3-540-46029-2_12","volume-title":"Computer Performance Evaluation: Modelling Techniques and Tools","author":"I Davies","year":"2002","unstructured":"Davies, I., Knottenbelt, W., Kritzinger, P.S.: Symbolic methods for the state space exploration of GSPN models. In: Field, T., Harrison, P.G., Bradley, J., Harder, U. (eds.) TOOLS 2002. LNCS, vol. 2324, pp. 188\u2013199. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-46029-2_12"},{"key":"16_CR17","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). https:\/\/doi.org\/10.1007\/978-3-319-41192-7"},{"unstructured":"Lind-Nielsen, J.: BuDDy Manual, July 2003. http:\/\/buddy.sourceforge.net\/manual\/main.html","key":"16_CR18"},{"issue":"1","key":"16_CR19","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. Multiple-Valued Logic 4(1), 9\u201362 (1992)","journal-title":"Multiple-Valued Logic"},{"issue":"4","key":"16_CR20","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":"16_CR21","series-title":"Informatik-Fachberichte","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/978-3-642-68353-4_47","volume-title":"Application and Theory of Petri Nets","author":"J Martinez","year":"1982","unstructured":"Martinez, J., Silva, M.: A simple and fast algorithm to obtain all invariants of a generalized Petri net. In: Girault, C., Reisig, W. (eds.) Application and Theory of Petri Nets. INFORMATIK, vol. 52, pp. 301\u2013310. Springer, Heidelberg (1982). https:\/\/doi.org\/10.1007\/978-3-642-68353-4_47"},{"key":"16_CR22","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 (1993)"},{"key":"16_CR23","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"},{"key":"16_CR24","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). https:\/\/doi.org\/10.1007\/11691372_6"},{"doi-asserted-by":"crossref","unstructured":"Smith, B., Ciardo, G.: SOUPS: a variable ordering metric for the saturation algorithm. In: Proceedings of the International Conference on Application of Concurrency to System Design (ACSD). IEEE Computer Society Press (2018)","key":"16_CR25","DOI":"10.1109\/ACSD.2018.000-4"},{"issue":"2","key":"16_CR26","doi-asserted-by":"crossref","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":"16_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/978-3-662-46681-0_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y Thierry-Mieg","year":"2015","unstructured":"Thierry-Mieg, Y.: Symbolic model-checking using ITS-tools. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 231\u2013237. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_20"},{"key":"16_CR28","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1016\/j.peva.2011.02.005","volume":"68","author":"M Wan","year":"2011","unstructured":"Wan, M., Ciardo, G., Miner, A.S.: Approximate steady-state analysis of large Markov models based on the structure of their decision diagram encoding. Perf. Eval. 68, 463\u2013486 (2011)","journal-title":"Perf. Eval."}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-17465-1_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,5]],"date-time":"2020-12-05T12:42:51Z","timestamp":1607172171000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-17465-1_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030174644","9783030174651"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-17465-1_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"3 April 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Prague","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Czech Republic","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2019\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"164","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"42","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"8","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"26% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"13","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"12 full papers and 11 short papers accepted for TOOLympics and SV-COMP (avg. 4 reviewers\/paper, selected from 43 submissions)","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}}]}}