{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,25]],"date-time":"2025-06-25T09:26:14Z","timestamp":1750843574828,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662653029"},{"type":"electronic","value":"9783662653036"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-662-65303-6_5","type":"book-chapter","created":{"date-parts":[[2022,4,19]],"date-time":"2022-04-19T06:02:49Z","timestamp":1650348169000},"page":"91-111","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Portfolio Management in\u00a0Explicit Model Checking"],"prefix":"10.1007","author":[{"given":"Karsten","family":"Wolf","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,4,20]]},"reference":[{"key":"5_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/978-3-540-47919-2_13","volume-title":"Petri Nets: Central Models and Their Properties","author":"G Berthelot","year":"1987","unstructured":"Berthelot, G.: Transformations and decompositions of nets. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) ACPN 1986. LNCS, vol. 254, pp. 359\u2013376. Springer, Heidelberg (1987). https:\/\/doi.org\/10.1007\/978-3-540-47919-2_13"},{"key":"5_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/978-3-319-91268-4_8","volume-title":"Application and Theory of Petri Nets and Concurrency","author":"F B\u00f8nneland","year":"2018","unstructured":"B\u00f8nneland, F., Dyhr, J., Jensen, P.G., Johannsen, M., Srba, J.: Simplification of CTL formulae for efficient model checking of Petri nets. In: Khomenko, V., Roux, O.H. (eds.) PETRI NETS 2018. LNCS, vol. 10877, pp. 143\u2013163. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-91268-4_8"},{"issue":"2","key":"5_CR3","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"JR Burch","year":"1992","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)","journal-title":"Inf. Comput."},{"issue":"2","key":"5_CR4","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"EM Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8(2), 244\u2013263 (1986)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"5_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"492","DOI":"10.1007\/978-3-642-28756-5_36","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A David","year":"2012","unstructured":"David, A., Jacobsen, L., Jacobsen, M., J\u00f8rgensen, K.Y., M\u00f8ller, M.H., Srba, J.: TAPAAL 2.0: integrated development environment for timed-arc Petri nets. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 492\u2013497. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28756-5_36"},{"key":"5_CR6","series-title":"Monographs in Theoretical Computer Science An EATCS Series","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-77426-6","volume-title":"Unfoldings - A Partial-Order Approach to Model Checking","author":"J Esparza","year":"2008","unstructured":"Esparza, J., Heljanko, K.: Unfoldings - A Partial-Order Approach to Model Checking. Monographs in Theoretical Computer Science An EATCS Series, Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-77426-6"},{"key":"5_CR7","unstructured":"Hack, M.H.T.: Analysis of production schemata by Petri nets. Master\u2019s thesis, MIT, Department of Electrical Engineering, Cambridge, Massachusetts (1972)"},{"issue":"1\/2","key":"5_CR8","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/BF00625967","volume":"9","author":"K Jensen","year":"1996","unstructured":"Jensen, K.: Condensed state spaces for symmetrical coloured Petri nets. Formal Methods Syst. Des. 9(1\/2), 7\u201340 (1996). https:\/\/doi.org\/10.1007\/BF00625967","journal-title":"Formal Methods Syst. Des."},{"key":"5_CR9","unstructured":"Kordon, F., et al.: Complete Results for the 2019 Edition of the Model Checking Contest, April 2019. http:\/\/mcc.lip6.fr\/2019\/results.php"},{"issue":"3","key":"5_CR10","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/s10703-006-0006-1","volume":"29","author":"LM Kristensen","year":"2006","unstructured":"Kristensen, L.M., Schmidt, K., Valmari, A.: Question-guided stubborn set methods for state properties. Formal Methods Syst. Des. 29(3), 215\u2013251 (2006). https:\/\/doi.org\/10.1007\/s10703-006-0006-1","journal-title":"Formal Methods Syst. Des."},{"key":"5_CR11","unstructured":"Liebke, T., Rosenke, C.: Faster enabledness-updates for the reachability graph computation. In: Proceedings of PNSE 2020, pp. 108\u2013117 (2020)"},{"key":"5_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/978-3-030-21571-2_18","volume-title":"Application and Theory of Petri Nets and Concurrency","author":"T Liebke","year":"2019","unstructured":"Liebke, T., Wolf, K.: Taking some burden off an explicit CTL model checker. In: Donatelli, S., Haar, S. (eds.) PETRI NETS 2019. LNCS, vol. 11522, pp. 321\u2013341. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-21571-2_18"},{"key":"5_CR13","unstructured":"Lipton, R.: The reachability problem requires exponential space. Technical report 62, Yale University (1976)"},{"key":"5_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/978-3-642-13675-7_16","volume-title":"Applications and Theory of Petri Nets","author":"O Oanea","year":"2010","unstructured":"Oanea, O., Wimmel, H., Wolf, K.: New algorithms for deciding the siphon-trap property. In: Lilius, J., Penczek, W. (eds.) PETRI NETS 2010. LNCS, vol. 6128, pp. 267\u2013286. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-13675-7_16"},{"issue":"7","key":"5_CR15","doi-asserted-by":"publisher","first-page":"545","DOI":"10.1007\/s002360050002","volume":"36","author":"K Schmidt","year":"2000","unstructured":"Schmidt, K.: How to calculate symmetries of Petri nets. Acta Informatica 36(7), 545\u2013590 (2000). https:\/\/doi.org\/10.1007\/s002360050002","journal-title":"Acta Informatica"},{"issue":"12","key":"5_CR16","doi-asserted-by":"publisher","first-page":"1307","DOI":"10.1109\/71.553301","volume":"7","author":"SM Shatz","year":"1996","unstructured":"Shatz, S.M., Tu, S., Murata, T., Duri, S.: An application of Petri net reduction for Ada tasking deadlock analysis. IEEE Trans. Parallel Distrib. Syst. 7(12), 1307\u20131322 (1996)","journal-title":"IEEE Trans. Parallel Distrib. Syst."},{"issue":"2","key":"5_CR17","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1137\/0201010","volume":"1","author":"RE Tarjan","year":"1972","unstructured":"Tarjan, R.E.: Depth-first search and linear graph algorithms. SIAM J. Comput. 1(2), 146\u2013160 (1972)","journal-title":"SIAM J. Comput."},{"key":"5_CR18","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":"5_CR19","unstructured":"Tovchigrechko, A.A.: Efficient symbolic analysis of bounded Petri nets using interval decision diagrams. Ph.D. thesis, Brandenburg University of Technology, Cottbus - Senftenberg, Germany (2008)"},{"key":"5_CR20","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":"5_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-3-662-55862-1_7","volume-title":"Transactions on Petri Nets and Other Models of Concurrency XII","author":"A Valmari","year":"2017","unstructured":"Valmari, A., Hansen, H.: Stubborn set intuition explained. In: Koutny, M., Kleijn, J., Penczek, W. (eds.) Transactions on Petri Nets and Other Models of Concurrency XII. LNCS, vol. 10470, pp. 140\u2013165. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-55862-1_7"},{"key":"5_CR22","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification (preliminary report). In: Proceedings of the Symposium on Logic in Computer Science. LICS, IEEE, pp. 332\u2013344 (1986)"},{"key":"5_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/3-540-57208-2_31","volume-title":"CONCUR 1993","author":"B Vergauwen","year":"1993","unstructured":"Vergauwen, B., Lewi, J.: A linear local model checking algorithm for CTL. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 447\u2013461. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/3-540-57208-2_31"},{"key":"5_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/10722167_13","volume-title":"Computer Aided Verification","author":"PF Williams","year":"2000","unstructured":"Williams, P.F., Biere, A., Clarke, E.M., Gupta, A.: Combining decision diagrams and SAT procedures for efficient symbolic model checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 124\u2013138. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10722167_13"},{"issue":"3","key":"5_CR25","first-page":"1","volume":"8","author":"H Wimmel","year":"2012","unstructured":"Wimmel, H., Wolf, K.: Applying CEGAR to the Petri net state equation. Log. Methods Comput. Sci. 8(3), 1\u201315 (2012)","journal-title":"Log. Methods Comput. Sci."},{"key":"5_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/978-3-662-53401-4_13","volume-title":"Transactions on Petri Nets and Other Models of Concurrency XI","author":"K Wolf","year":"2016","unstructured":"Wolf, K.: Running LoLA 2.0 in a model checking competition. In: Koutny, M., Desel, J., Kleijn, J. (eds.) Transactions on Petri Nets and Other Models of Concurrency XI. LNCS, vol. 9930, pp. 274\u2013285. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-53401-4_13"},{"key":"5_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/978-3-319-91268-4_18","volume-title":"Application and Theory of Petri Nets and Concurrency","author":"K Wolf","year":"2018","unstructured":"Wolf, K.: Petri net model checking with LoLA 2. In: Khomenko, V., Roux, O.H. (eds.) PETRI NETS 2018. LNCS, vol. 10877, pp. 351\u2013362. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-91268-4_18"}],"container-title":["Lecture Notes in Computer Science","Transactions on Petri Nets and Other Models of Concurrency XVI"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-65303-6_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,4,19]],"date-time":"2022-04-19T06:03:27Z","timestamp":1650348207000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-662-65303-6_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783662653029","9783662653036"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-65303-6_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"20 April 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}