{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,3]],"date-time":"2026-10-03T18:25:51Z","timestamp":1791051951495,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":47,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540730934","type":"print"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73094-1_5","type":"book-chapter","created":{"date-parts":[[2007,6,30]],"date-time":"2007-06-30T05:53:56Z","timestamp":1183182836000},"page":"29-42","source":"Crossref","is-referenced-by-count":53,"title":["Generating Petri Net State Spaces"],"prefix":"10.1007","author":[{"given":"Karsten","family":"Wolf","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"5_CR1","doi-asserted-by":"crossref","unstructured":"Berthelot, G.: Checking properties of nets using transformations. Advances in Petri Nets, pp. 19\u201340 (1986)","DOI":"10.1007\/BFb0016204"},{"key":"5_CR2","doi-asserted-by":"crossref","unstructured":"Chiola, G., Dutheillet, C., Franceschinis, G., Haddad, S.: On well\u2013formed colored nets and their symbolic reachability graph. In: Proc. ICATPN, pp. 378\u2013410 (1990)","DOI":"10.1007\/978-3-642-84524-6_13"},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logic of Programs","author":"E.M. Clarke","year":"1981","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronisation skeletons using brnaching tim temporal logic. In: Logic of Programs. LNCS, vol.\u00a0131, pp. 52\u201371. Springer, Heidelberg (1981)"},{"key":"5_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"450","DOI":"10.1007\/3-540-45319-9_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Christensen","year":"2001","unstructured":"Christensen, S., Kristensen, L.M., Mailund, T.: A sweep-line method for state space exploration. In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol.\u00a02031, pp. 450\u2013464. Springer, Heidelberg (2001)"},{"key":"5_CR5","unstructured":"Commoner, F.: Deadlocks in Petri nets. Technical report, Applied Data Research Inc. Wakefield, Massachussetts (1972)"},{"key":"5_CR6","unstructured":"Curbera, F., et al.: Business process execution language for web services, version 1.1. Technical report, BEA, IBM, Microsoft (2003)"},{"key":"5_CR7","doi-asserted-by":"publisher","first-page":"522","DOI":"10.1109\/ICCD.1992.276232","volume-title":"Proc. IEEE Int. Conf. Computer Design: VLSI in Computers and Processors","author":"D.L. Dill","year":"1992","unstructured":"Dill, D.L., Drexler, A.J., Hu, A.J., Yang, C.H.: Protocol verification as a hardware design aid. In: Proc. IEEE Int. Conf. Computer Design: VLSI in Computers and Processors, pp. 522\u2013525. IEEE Computer Society Press, Los Alamitos (1992)"},{"key":"5_CR8","volume-title":"Handbook of Theoretical Computer Science","author":"E.A. Emerson","year":"1990","unstructured":"Emerson, E.A.: Handbook of Theoretical Computer Science, Ch. 16. Elsevier, Amsterdam (1990)"},{"key":"5_CR9","unstructured":"Esparza, J.: Model checking using net unfoldings. Technical Report 14\/92, Universit\u00e4t Hildesheim (1992)"},{"key":"5_CR10","unstructured":"Finkel, A.: A minimal coverability graph for Petri nets. In: Proc. ICATPN, pp. 1\u201321 (1990)"},{"key":"5_CR11","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1109\/ISTCS.1995.377038","volume-title":"Symp. on the Theory of Computing and Systems","author":"R. Gerth","year":"1995","unstructured":"Gerth, R., Kuiper, R., Peled, D., Penczek, W.: A partial order approach to branching time logic model checking. In: Symp. on the Theory of Computing and Systems, pp. 130\u2013140. IEEE Computer Society Press, Los Alamitos (1995)"},{"key":"5_CR12","doi-asserted-by":"crossref","first-page":"98","DOI":"10.1007\/978-3-642-69028-0_8","volume":"66","author":"H. Genrich","year":"1983","unstructured":"Genrich, H., Lautenbach, K.: S\u2013invariance in Pr\/T\u2013nets. Informatik\u2013Fachberichte\u00a066, 98\u2013111 (1983)","journal-title":"Informatik\u2013Fachberichte"},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Wolper, P.: A partial approach to model checking. In: IEEE Symp. on Logic in Computer Science, pp. 406\u2013415 (1991)","DOI":"10.1109\/LICS.1991.151664"},{"key":"5_CR14","volume-title":"Design an Validation of Computer Protocols","author":"G. Holzmann","year":"1991","unstructured":"Holzmann, G.: Design an Validation of Computer Protocols. Prentice-Hall, Englewood Cliffs (1991)"},{"key":"5_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/11538394_15","volume-title":"Business Process Management","author":"S. Hinz","year":"2005","unstructured":"Hinz, S., Schmidt, K., Stahl, C.: Transforming BPEL to Petri nets. In: van der Aalst, W.M.P., Benatallah, B., Casati, F., Curbera, F. (eds.) BPM 2005. LNCS, vol.\u00a03649, pp. 220\u2013235. Springer, Heidelberg (2005)"},{"key":"5_CR16","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1016\/0304-3975(81)90049-9","volume":"14","author":"K. Jensen","year":"1981","unstructured":"Jensen, K.: Coloured Petri nets and the invariant method. Theoretical Computer Science\u00a014, 317\u2013336 (1981)","journal-title":"Theoretical Computer Science"},{"key":"5_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"258","DOI":"10.1007\/978-3-540-27793-4_15","volume-title":"Applications and Theory of Petri Nets 2004","author":"T. Junttila","year":"2004","unstructured":"Junttila, T.: New canonical representative marking algorithms for place\/transition nets. In: Cortadella, J., Reisig, W. (eds.) ICATPN 2004. LNCS, vol.\u00a03099, pp. 258\u2013277. Springer, Heidelberg (2004)"},{"key":"5_CR18","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1016\/S0022-0000(69)80011-5","volume":"4","author":"R.M. Karp","year":"1969","unstructured":"Karp, R.M., Miller, R.E.: Parallel programm schemata. Journ. Computer and System Sciences\u00a04, 147\u2013195 (1969)","journal-title":"Journ. Computer and System Sciences"},{"key":"5_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"549","DOI":"10.1007\/3-540-45614-7_31","volume-title":"FME 2002: Formal Methods - Getting IT Right","author":"L.M. Kristensen","year":"2002","unstructured":"Kristensen, L.M., Mailund, T.: A generalized sweep-line method for safety properties. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol.\u00a02391, pp. 549\u2013567. Springer, Heidelberg (2002)"},{"key":"5_CR20","series-title":"Lecture Notes in Computer Science","volume-title":"Application and Theory of Petri Nets 1999","author":"F. Kordon","year":"1999","unstructured":"Kordon, F., Paviot-Adet, E.: Using CPN-AMI to validate a sfae channel protocol. In: Donatelli, S., Kleijn, J.H.C.M. (eds.) ICATPN 1999. LNCS, vol.\u00a01639, Springer, Heidelberg (1999)"},{"issue":"3","key":"5_CR21","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/s10703-006-0006-1","volume":"29","author":"L. Kristensen","year":"2006","unstructured":"Kristensen, L., Schmidt, K., Valmari, A.: Question-guided stubborn set methods for state properties. Formal Methods in System Design\u00a029(3), 215\u2013251 (2006)","journal-title":"Formal Methods in System Design"},{"key":"5_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"282","DOI":"10.1007\/3-540-44988-4_17","volume-title":"Application and Theory of Petri Nets 2000","author":"L.M. Krisensen","year":"2000","unstructured":"Krisensen, L.M., Valmari, A.: Improved question-guided stubborn set methods for state properties. In: Nielsen, M., Simpson, D. (eds.) ICATPN 2000. LNCS, vol.\u00a01825, pp. 282\u2013302. Springer, Heidelberg (2000)"},{"issue":"4","key":"5_CR23","doi-asserted-by":"crossref","first-page":"486","DOI":"10.1007\/s100090100055","volume":"3","author":"E. Kindler","year":"2001","unstructured":"Kindler, E., Weber, M.: The Petri net kernel - an infrastructure for building petri net tools. STTT\u00a03(4), 486\u2013497 (2001)","journal-title":"STTT"},{"key":"5_CR24","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1109\/REAL.1997.641265","volume-title":"Proc. IEEE Real-Time Systems Symp.","author":"K.G. Larsen","year":"1997","unstructured":"Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: Efficient verification of real-time systems: compact data structure and state-space reduction. In: Proc. IEEE Real-Time Systems Symp., pp. 14\u201324. IEEE Computer Society Press, Los Alamitos (1997)"},{"key":"5_CR25","unstructured":"Lautenbach, K., Schmidt, H.A.: Use of Petri nets for proving correctness of concurrent process systems. In: IFIP Congress, pp. 187\u2013191 (1974)"},{"key":"5_CR26","unstructured":"McMillan, K.: The SMV homepage. http:\/\/www.cad.eecs.berkeley.edu\/~kenmcmil\/smv\/"},{"key":"5_CR27","unstructured":"Mailund, T.: Sweeping the State Space - a sweep-line state space exploration method. PhD thesis, University of Aarhus (2003)"},{"key":"5_CR28","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems","author":"Z. Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems (Specification), vol.\u00a01. Springer, Heidelberg (1992)"},{"key":"5_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"164","DOI":"10.1007\/3-540-56496-9_14","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"1993","unstructured":"McMillan, K.L.: Using unfoldings to avoid the state explosion problem in the verification of asynchronious circuits. In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol.\u00a0663, pp. 164\u2013177. Springer, Heidelberg (1993)"},{"key":"5_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"409","DOI":"10.1007\/3-540-56922-7_34","volume-title":"Computer Aided Verification","author":"D. Peled","year":"1993","unstructured":"Peled, D.: All from one, one for all: on model\u2013checking using representitives. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol.\u00a0697, pp. 409\u2013423. Springer, Heidelberg (1993)"},{"key":"5_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","volume-title":"International Symposium on Programming","author":"J.P. Quielle","year":"1982","unstructured":"Quielle, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) International Symposium on Programming. LNCS, vol.\u00a0137, pp. 337\u2013351. Springer, Heidelberg (1982)"},{"key":"5_CR32","unstructured":"Roch, S., Starke, P.: INA Integrierter Netz Analysator Version 2.1. Technical Report 102, Humboldt\u2013Universit\u00e4t zu Berlin (1998)"},{"key":"5_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"46","DOI":"10.1007\/3-540-48745-X_4","volume-title":"Application and Theory of Petri Nets 1999","author":"K. Schmidt","year":"1999","unstructured":"Schmidt, K.: Stubborn set for standard properties. In: Donatelli, S., Kleijn, J.H.C.M. (eds.) ICATPN 1999. LNCS, vol.\u00a01639, pp. 46\u201365. Springer, Heidelberg (1999)"},{"key":"5_CR34","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\u00a036, 545\u2013590 (2000)","journal-title":"Acta Informatica"},{"key":"5_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"315","DOI":"10.1007\/3-540-46419-0_22","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. Schmidt","year":"2000","unstructured":"Schmidt, K.: Integrating low level symmetries into reachability analysis. In: Schwartzbach, M.I., Graf, S. (eds.) ETAPS 2000 and TACAS 2000. LNCS, vol.\u00a01785, pp. 315\u2013331. Springer, Heidelberg (2000)"},{"key":"5_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1007\/3-540-44988-4_27","volume-title":"Application and Theory of Petri Nets 2000","author":"K. Schmidt","year":"2000","unstructured":"Schmidt, K.: LoLA \u2013 a low level analyzer. In: Nielsen, M., Simpson, D. (eds.) ICATPN 2000. LNCS, vol.\u00a01825, pp. 465\u2013474. Springer, Heidelberg (2000)"},{"issue":"1-4","key":"5_CR37","first-page":"331","volume":"43","author":"K. Schmidt","year":"2000","unstructured":"Schmidt, K.: Stubborn set for modelchecking the EF\/AG fragment of CTL. Fundamenta Informaticae\u00a043(1-4), 331\u2013341 (2000)","journal-title":"Fundamenta Informaticae"},{"key":"5_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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 invariantsin state space construction. In: Garavel, H., Hatcliff, J. (eds.) ETAPS 2003 and TACAS 2003. LNCS, vol.\u00a02619, pp. 473\u2013488. Springer, Heidelberg (2003)"},{"key":"5_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"192","DOI":"10.1007\/978-3-540-24730-2_17","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. Schmidt","year":"2004","unstructured":"Schmidt, K.: Automated generation of a progress measure for the sweep-line method. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 192\u2013204. Springer, Heidelberg (2004)"},{"key":"5_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"463","DOI":"10.1007\/3-540-44919-1_29","volume-title":"Applications and Theory of Petri Nets 2003","author":"C. Schr\u00f6ter","year":"2003","unstructured":"Schr\u00f6ter, C., Schwoon, S., Esparza, J.: The Model-Checking Kit. In: van der Aalst, W.M.P., Best, E. (eds.) ICATPN 2003. LNCS, vol.\u00a02679, pp. 463\u2013472. Springer, Heidelberg (2003)"},{"key":"5_CR41","doi-asserted-by":"crossref","unstructured":"Stahl, C., Reisig, W., Krstic, M.: Hazard detection in a GALS wrapper: A case study. In: Proc. ACSD, pp. 234\u2013243 (2005)","DOI":"10.1109\/ACSD.2005.20"},{"key":"5_CR42","first-page":"294","volume":"8","author":"P. Starke","year":"1991","unstructured":"Starke, P.: Reachability analysis of Petri nets using symmetries. J. Syst. Anal. Model. Simul.\u00a08, 294\u2013303 (1991)","journal-title":"J. Syst. Anal. Model. Simul."},{"key":"5_CR43","unstructured":"Talcott, C.: Personal communication. Dagstuhl Seminar (2007)"},{"key":"5_CR44","unstructured":"Reisig, W., et al.: The homepage of the project Tools4BPEL. http:\/\/www2.informatik.hu-berlin.de\/top\/forschung\/projekte\/tools4bpel\/"},{"key":"5_CR45","unstructured":"Valmari, A.: Error detection by reduced reachability graph generation. ICATPN (1988)"},{"key":"5_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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.) Advances in Petri Nets 1990. LNCS, vol.\u00a0483, pp. 491\u2013511. Springer, Heidelberg (1991)"},{"key":"5_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1007\/3-540-56922-7_6","volume-title":"Computer Aided Verification","author":"P. Wolper","year":"1993","unstructured":"Wolper, P., Leroy, D.: Reliable hashing without collision detection. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol.\u00a0697, pp. 59\u201370. Springer, Heidelberg (1993)"}],"container-title":["Lecture Notes in Computer Science","Petri Nets and Other Models of Concurrency \u2013 ICATPN 2007"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73094-1_5.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T05:11:51Z","timestamp":1605762711000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73094-1_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540730934"],"references-count":47,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73094-1_5","relation":{},"subject":[]}}