{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,7]],"date-time":"2025-06-07T08:10:10Z","timestamp":1749283810631,"version":"3.41.0"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031946332","type":"print"},{"value":"9783031946349","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-94634-9_23","type":"book-chapter","created":{"date-parts":[[2025,6,7]],"date-time":"2025-06-07T07:59:31Z","timestamp":1749283171000},"page":"478-500","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Symbolic Model Checking in\u00a0the\u00a0Modular State Space Using Binary Decision Diagrams"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0003-7022-6021","authenticated-orcid":false,"given":"Lukas","family":"Zech","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,6,8]]},"reference":[{"key":"23_CR1","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1613\/jair.3653","volume":"45","author":"I Ab\u00edo","year":"2012","unstructured":"Ab\u00edo, I., Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-Carbonell, E., Mayer-Eichberger, V.: A new look at BDDs for pseudo-boolean constraints. J. Artif. Intell. Res. 45, 443\u2013480 (2012). https:\/\/doi.org\/10.1613\/jair.3653","journal-title":"J. Artif. Intell. Res."},{"key":"23_CR2","doi-asserted-by":"publisher","unstructured":"Amparore, E., et al.: Presentation of the 9th edition of the model checking contest. In: Beyer, D., Huisman, M., Kordon, F., Steffen, B. (eds.) TACAS 2019. LNCS, vol. 11429, pp. 50\u201368. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17502-3_4","DOI":"10.1007\/978-3-030-17502-3_4"},{"key":"23_CR3","doi-asserted-by":"publisher","unstructured":"Amparore, E.G., Donatelli, S., Beccuti, M., Garbi, G., Miner, A.: Decision diagrams for petri nets: a comparison of variable ordering algorithms. In: Koutny, M., Kristensen, L.M., Penczek, W. (eds.) Transactions on Petri Nets and Other Models of Concurrency XIII. LNCS, vol. 11090, pp. 73\u201392. Springer, Heidelberg (2018). https:\/\/doi.org\/10.1007\/978-3-662-58381-4_4","DOI":"10.1007\/978-3-662-58381-4_4"},{"issue":"1","key":"23_CR4","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/0304-3975(94)00181-H","volume":"145","author":"Y Breitbart","year":"1995","unstructured":"Breitbart, Y., Hunt, H., Rosenkrantz, D.: On the size of binary decision diagrams representing Boolean functions. Theoret. Comput. Sci. 145(1), 45\u201369 (1995). https:\/\/doi.org\/10.1016\/0304-3975(94)00181-H","journal-title":"Theoret. Comput. Sci."},{"issue":"3","key":"23_CR5","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"RE Bryant","year":"1992","unstructured":"Bryant, R.E.: Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Comput. Surv. 24(3), 293\u2013318 (1992). https:\/\/doi.org\/10.1145\/136035.136043","journal-title":"ACM Comput. Surv."},{"key":"23_CR6","doi-asserted-by":"publisher","unstructured":"Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. C-35, 677\u2013691 (1986). https:\/\/doi.org\/10.1109\/TC.1986.1676819","DOI":"10.1109\/TC.1986.1676819"},{"issue":"3","key":"23_CR7","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1023\/A:1015669415634","volume":"12","author":"P Buchholz","year":"2002","unstructured":"Buchholz, P., Kemper, P.: Efficient computation and representation of large reachability sets for composed automata. Discrete Event Dyn. Syst. 12(3), 265\u2013286 (2002). https:\/\/doi.org\/10.1023\/A:1015669415634","journal-title":"Discrete Event Dyn. Syst."},{"issue":"3","key":"23_CR8","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1023\/A:1020321222420","volume":"21","author":"P Buchholz","year":"2002","unstructured":"Buchholz, P., Kemper, P.: Hierarchical reachability graph generation for petri nets. Formal Methods Syst. Des. 21(3), 281\u2013315 (2002). https:\/\/doi.org\/10.1023\/A:1020321222420","journal-title":"Formal Methods Syst. Des."},{"key":"23_CR9","doi-asserted-by":"publisher","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 10$$^{20}$$ states and beyond. Inf. Comput. 98(2), 142\u2013170 (1992). https:\/\/doi.org\/10.1016\/0890-5401(92)90017-A","DOI":"10.1016\/0890-5401(92)90017-A"},{"issue":"3","key":"23_CR10","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1093\/comjnl\/43.3.224","volume":"43","author":"S Christensen","year":"2000","unstructured":"Christensen, S., Petrucci, L.: Modular analysis of petri nets. Comput. J. 43(3), 224\u2013242 (2000). https:\/\/doi.org\/10.1093\/comjnl\/43.3.224","journal-title":"Comput. J."},{"key":"23_CR11","doi-asserted-by":"crossref","unstructured":"Ciardo, G., L\u00fcttgen, G., Siminiceanu, R.: Saturation: an efficient iteration strategy for symbolic state-space generation. In: Goos, G., Hartmanis, J., Van Leeuwen, J., Margaria, T., Yi, W. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, vol. 2031, pp. 328\u2013342. Springer, Heidelberg (2001)","DOI":"10.1007\/3-540-45319-9_23"},{"issue":"1","key":"23_CR12","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/BF00625969","volume":"9","author":"EM Clarke","year":"1996","unstructured":"Clarke, E.M., Enders, R., Filkorn, T., Jha, S.: Exploiting symmetry in temporal logic model checking. Formal Methods Syst. Des. 9(1), 77\u2013104 (1996). https:\/\/doi.org\/10.1007\/BF00625969","journal-title":"Formal Methods Syst. Des."},{"key":"23_CR13","doi-asserted-by":"publisher","unstructured":"Classen, A., Heymans, P., Schobbens, P.Y., Legay, A.: Symbolic model checking of software product lines. In: Proceedings of the 33rd International Conference on Software Engineering, ICSE 2011, pp. 321\u2013330. Association for Computing Machinery, New York (2011). https:\/\/doi.org\/10.1145\/1985793.1985838","DOI":"10.1145\/1985793.1985838"},{"key":"23_CR14","doi-asserted-by":"publisher","unstructured":"van Dijk, T., van de Pol, J.: Sylvan: multi-core decision diagrams. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 677\u2013691. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_60","DOI":"10.1007\/978-3-662-46681-0_60"},{"issue":"2","key":"23_CR15","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1023\/A:1008743212620","volume":"16","author":"J Esparza","year":"2000","unstructured":"Esparza, J., Melzer, S.: Verification of safety properties using integer programming: beyond the state equation. Formal Methods Syst. Des. 16(2), 159\u2013189 (2000). https:\/\/doi.org\/10.1023\/A:1008743212620","journal-title":"Formal Methods Syst. Des."},{"key":"23_CR16","doi-asserted-by":"publisher","unstructured":"Friedman, S.J., Supowit, K.J.: Finding the optimal variable ordering for binary decision diagrams. In: Proceedings of the 24th ACM\/IEEE Design Automation Conference, DAC 1987, pp. 348\u2013356. Association for Computing Machinery, New York (1987). https:\/\/doi.org\/10.1145\/37888.37941","DOI":"10.1145\/37888.37941"},{"key":"23_CR17","unstructured":"Gaede, J., Overath, J., Wallner, S.: Automatic modularization of place\/transition nets. In: K\u00f6hler-Bussmeier, M., Moldt, D., R\u00f6lke, H. (eds.) Proceedings of the International Workshop on Petri Nets and Software Engineering 2024 co-located with the 45th International Conference on Application and Theory of Petri Nets and Concurrency (PETRI NETS 2024), 24\u201325 June 2024, Geneva, Switzerland. CEUR Workshop Proceedings, vol.\u00a03730, pp. 53\u201373. CEUR-WS.org (2024). https:\/\/ceur-ws.org\/Vol-3730\/paper03.pdf"},{"key":"23_CR18","doi-asserted-by":"publisher","unstructured":"Gaede, J., Wallner, S., Wolf, K.: Modular state spaces - a new perspective. In: Kristensen, L.M., van\u00a0der Werf, J.M. (eds.) Application and Theory of Petri Nets and Concurrency, pp. 312\u2013332. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-61433-0_15","DOI":"10.1007\/978-3-031-61433-0_15"},{"key":"23_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/BFb0023731","volume-title":"Computer-Aided Verification","author":"P Godefroid","year":"1991","unstructured":"Godefroid, P.: Using partial orders to improve automatic verification methods. In: Clarke, E.M., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 176\u2013185. Springer, Heidelberg (1991). https:\/\/doi.org\/10.1007\/BFb0023731"},{"key":"23_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"186","DOI":"10.1007\/BFb0023732","volume-title":"Computer-Aided Verification","author":"S Graf","year":"1991","unstructured":"Graf, S., Steffen, B.: Compositional minimization of finite state systems. In: Clarke, E.M., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 186\u2013196. Springer, Heidelberg (1991). https:\/\/doi.org\/10.1007\/BFb0023732"},{"key":"23_CR21","doi-asserted-by":"publisher","unstructured":"He, L., Liu, G.: Petri net based CTL model checking: using a new method to construct OBDD variable order. In: 2021 International Symposium on Theoretical Aspects of Software Engineering (TASE), pp. 159\u2013166 (2021). https:\/\/doi.org\/10.1109\/TASE52547.2021.00033","DOI":"10.1109\/TASE52547.2021.00033"},{"key":"23_CR22","unstructured":"Le\u00a0Cornec, Y.S.: Compositional analysis of modular Petri nets using hierarchical state space abstraction. In: Joint 5th International Workshop on Logics, Agents, and Mobility, LAM 2012, the 1st International Workshop on Petri Net-Based Security, WooPS 2012 and the 2nd International Workshop on Petri Nets Compositions, CompoNet 2012. CEUR Workshop Proceedings, Hamburg, Germany, vol.\u00a0853, pp. 119\u2013133 (2012). https:\/\/hal.archives-ouvertes.fr\/hal-00785569"},{"key":"23_CR23","doi-asserted-by":"publisher","unstructured":"Lee, C.Y.: Representation of switching circuits by binary-decision programs. Bell Syst. Tech. J. 38, 985\u2013999 (1959). https:\/\/doi.org\/10.1002\/j.1538-7305.1959.tb01585.x","DOI":"10.1002\/j.1538-7305.1959.tb01585.x"},{"issue":"2","key":"23_CR24","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1109\/TSMC.1987.4309041","volume":"17","author":"H Lee-Kwang","year":"1987","unstructured":"Lee-Kwang, H., Favrel, J., Baptiste, P.: Generalized petri net reduction method. IEEE Trans. Syst. Man Cybern. 17(2), 297\u2013303 (1987). https:\/\/doi.org\/10.1109\/TSMC.1987.4309041","journal-title":"IEEE Trans. Syst. Man Cybern."},{"key":"23_CR25","unstructured":"Lind-Nielsen, J.: BuDDy: A binary decision diagram package. Report, Department of Information Technology Denmark (1999). https:\/\/buddy.sourceforge.net\/manual\/main.html"},{"key":"23_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1007\/3-540-48745-X_2","volume-title":"Application and Theory of Petri Nets 1999","author":"AS Miner","year":"1999","unstructured":"Miner, A.S., Ciardo, G.: Efficient reachability set generation and storage using decision diagrams. In: Donatelli, S., Kleijn, J. (eds.) ICATPN 1999. LNCS, vol. 1639, pp. 6\u201325. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48745-X_2"},{"key":"23_CR27","doi-asserted-by":"publisher","DOI":"10.1016\/j.softx.2024.101715","volume":"26","author":"M Mrena","year":"2024","unstructured":"Mrena, M., Kvassay, M., Zaitseva, E.: TeDDy: templated decision diagram library. SoftwareX 26, 101715 (2024). https:\/\/doi.org\/10.1016\/j.softx.2024.101715","journal-title":"SoftwareX"},{"key":"23_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/978-3-540-30476-0_11","volume-title":"Automated Technology for Verification and Analysis","author":"S Ogata","year":"2004","unstructured":"Ogata, S., Tsuchiya, T., Kikuno, T.: SAT-based verification of safe petri nets. In: Wang, F. (ed.) ATVA 2004. LNCS, vol. 3299, pp. 79\u201392. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30476-0_11"},{"key":"23_CR29","doi-asserted-by":"publisher","first-page":"432","DOI":"10.1109\/12.926158","volume":"50","author":"E Pastor","year":"2001","unstructured":"Pastor, E., Cortadella, J., Roig, O.: Symbolic analysis of bounded Petri nets. IEEE Trans. Comput. 50, 432\u2013448 (2001). https:\/\/doi.org\/10.1109\/12.926158","journal-title":"IEEE Trans. Comput."},{"issue":"2","key":"23_CR30","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/s10470-011-9773-8","volume":"74","author":"G Shi","year":"2013","unstructured":"Shi, G.: A survey on binary decision diagram approaches to symbolic analysis of analog integrated circuits. Analog Integr. Circ. Sig. Process 74(2), 331\u2013343 (2013). https:\/\/doi.org\/10.1007\/s10470-011-9773-8","journal-title":"Analog Integr. Circ. Sig. Process"},{"key":"23_CR31","unstructured":"Somenzi, F.: CUDD: CU decision diagram package. Public Software, University of Colorado (1997). https:\/\/cir.nii.ac.jp\/crid\/1570009749922215168"},{"key":"23_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/3-540-53863-1_36","volume-title":"Advances in Petri Nets 1990","author":"A Valmari","year":"1991","unstructured":"Valmari, A.: Stubborn sets for reduced state space generation. In: Rozenberg, G. (ed.) ICATPN 1989. LNCS, vol. 483, pp. 491\u2013515. Springer, Heidelberg (1991). https:\/\/doi.org\/10.1007\/3-540-53863-1_36"},{"key":"23_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"531","DOI":"10.1007\/3-540-58152-9_29","volume-title":"Application and Theory of Petri Nets 1994","author":"A Valmari","year":"1994","unstructured":"Valmari, A.: Compositional analysis with place-bordered subnets. In: Valette, R. (ed.) ICATPN 1994. LNCS, vol. 815, pp. 531\u2013547. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-58152-9_29"},{"key":"23_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1007\/3-540-65306-6_21","volume-title":"Lectures on Petri Nets I: Basic Models","author":"A Valmari","year":"1998","unstructured":"Valmari, A.: The state explosion problem. In: Reisig, W., Rozenberg, G. (eds.) ACPN 1996. LNCS, vol. 1491, pp. 429\u2013528. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/3-540-65306-6_21"},{"key":"23_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"400","DOI":"10.1007\/978-3-642-38697-8_22","volume-title":"Application and Theory of Petri Nets and Concurrency","author":"M Westergaard","year":"2013","unstructured":"Westergaard, M.: CPN tools 4: multi-formalism and extensibility. In: Colom, J.-M., Desel, J. (eds.) PETRI NETS 2013. LNCS, vol. 7927, pp. 400\u2013409. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38697-8_22"},{"key":"23_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1007\/978-3-642-19835-9_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H Wimmel","year":"2011","unstructured":"Wimmel, H., Wolf, K.: Applying CEGAR to the petri net state equation. In: Abdulla, P.A., Leino, K. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 224\u2013238. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19835-9_19"},{"key":"23_CR37","doi-asserted-by":"publisher","unstructured":"Wolf, K.: Petri net model checking with LoLA 2. In: Khomenko, V., Roux, O.H. (eds.) Application and Theory of Petri Nets and Concurrency, pp. 351\u2013362. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-91268-4_18. https:\/\/git.informatik.uni-rostock.de\/theo\/lola-2","DOI":"10.1007\/978-3-319-91268-4_18"},{"key":"23_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/3-540-57208-2_17","volume-title":"CONCUR\u201993","author":"P Wolper","year":"1993","unstructured":"Wolper, P., Godefroid, P.: Partial-order methods for temporal verification. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 233\u2013246. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/3-540-57208-2_17"},{"key":"23_CR39","doi-asserted-by":"publisher","unstructured":"Zech, L., Wolf, K.: Verifying temporal logic properties in the modular state space. In: Kristensen, L.M., van\u00a0der Werf, J.M. (eds.) Application and Theory of Petri Nets and Concurrency, pp. 333\u2013354. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-61433-0_16","DOI":"10.1007\/978-3-031-61433-0_16"}],"container-title":["Lecture Notes in Computer Science","Application and Theory of Petri Nets and Concurrency"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-94634-9_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,7]],"date-time":"2025-06-07T07:59:33Z","timestamp":1749283173000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-94634-9_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031946332","9783031946349"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-94634-9_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"8 June 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"PETRI NETS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Applications and Theory of Petri Nets and Concurrency","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 June 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 June 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"46","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"apn2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf-2025.petrinet.net","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}