{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,19]],"date-time":"2026-10-19T17:15:44Z","timestamp":1792430144926,"version":"4.5.0"},"publisher-location":"Berlin, Heidelberg","reference-count":58,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662606506","type":"print"},{"value":"9783662606513","type":"electronic"}],"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-662-60651-3_2","type":"book-chapter","created":{"date-parts":[[2019,11,20]],"date-time":"2019-11-20T01:04:25Z","timestamp":1574211865000},"page":"36-63","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["How Petri Net Theory Serves Petri Net Model Checking: A Survey"],"prefix":"10.1007","author":[{"given":"Karsten","family":"Wolf","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2019,11,21]]},"reference":[{"key":"2_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"433","DOI":"10.1007\/978-3-540-45069-6_40","volume-title":"Computer Aided Verification","author":"G Behrmann","year":"2003","unstructured":"Behrmann, G., Larsen, K.G., Pel\u00e1nek, R.: To store or not to store. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 433\u2013445. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45069-6_40"},{"key":"2_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":"3","key":"2_CR3","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)","journal-title":"ACM Comput. Surv."},{"key":"2_CR4","unstructured":"B\u00fcchi, J.R.: On a decision method in restricted second order arithmetic. In: Proceedings of the International Congress on Logic, Method, and Philosophy of Science, pp. 1\u201312 (1962)"},{"key":"2_CR5","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 10$$^{20}$$ states and beyond. In: Proceedings of the LICS, pp. 428\u2013439. IEEE (1990)"},{"key":"2_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.) TACAS 2001. LNCS, vol. 2031, pp. 450\u2013464. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45319-9_31"},{"issue":"1","key":"2_CR7","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"EM Clarke","year":"2001","unstructured":"Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods Syst. Des. 19(1), 7\u201334 (2001)","journal-title":"Formal Methods Syst. Des."},{"issue":"2","key":"2_CR8","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."},{"issue":"5","key":"2_CR9","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1016\/S0022-0000(71)80013-2","volume":"5","author":"F Commoner","year":"1971","unstructured":"Commoner, F., Holt, A.W., Even, S., Pnueli, A.: Marked directed graphs. J. Comput. Syst. Sci. 5(5), 511\u2013523 (1971)","journal-title":"J. Comput. Syst. Sci."},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"Cook, S.A.: The complexity of theorem-proving procedures. In: Proceedings of the 3rd Annual ACM Symposium on Theory of Computing, pp. 151\u2013158 (1971)","DOI":"10.1145\/800157.805047"},{"issue":"3","key":"2_CR11","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1016\/0167-6423(83)90017-5","volume":"2","author":"EA Emerson","year":"1982","unstructured":"Emerson, E.A., Clarke, E.M.: Using branching time temporal logic to synthesize synchronization skeletons. Sci. Comput. Program. 2(3), 241\u2013266 (1982)","journal-title":"Sci. Comput. Program."},{"key":"2_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"613","DOI":"10.1007\/3-540-56610-4_93","volume-title":"TAPSOFT 1993: Theory and Practice of Software Development","author":"J Esparza","year":"1993","unstructured":"Esparza, J.: Model checking using net unfoldings. In: Gaudel, M.-C., Jouannaud, J.-P. (eds.) CAAP 1993. LNCS, vol. 668, pp. 613\u2013628. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/3-540-56610-4_93"},{"key":"2_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-63139-9_26","volume-title":"Application and Theory of Petri Nets 1997","author":"J Esparza","year":"1997","unstructured":"Esparza, J., Melzer, S.: Model checking LTL using constraint programming. In: Az\u00e9ma, P., Balbo, G. (eds.) ICATPN 1997. LNCS, vol. 1248, pp. 1\u201320. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/3-540-63139-9_26"},{"issue":"1","key":"2_CR14","doi-asserted-by":"crossref","first-page":"27","DOI":"10.3233\/FI-2014-1003","volume":"131","author":"S Evangelista","year":"2014","unstructured":"Evangelista, S., Kristensen, L.M.: A sweep-line method for B\u00fcchi automata-based model checking. Fundam. Inform. 131(1), 27\u201353 (2014)","journal-title":"Fundam. Inform."},{"key":"2_CR15","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":"2_CR16","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1006\/inco.1994.1035","volume":"110","author":"P Godefroid","year":"1994","unstructured":"Godefroid, P., Wolper, P.: A partial approach to model checking. Inf. Comput. 110(2), 305\u2013326 (1994)","journal-title":"Inf. Comput."},{"key":"2_CR17","unstructured":"Hack, M.: Analysis of production schemata by Petri nets. Technical report, MS thesis, Department of Electrical Engineering, MIT, Cambridge, Massachusetts (1972)"},{"key":"2_CR18","unstructured":"Hack, M.: Decidability questions for Petri nets. Outstanding Dissertations in the Computer Sciences. Garland Publishing, New York (1975)"},{"key":"2_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/978-3-319-19488-2_16","volume-title":"Application and Theory of Petri Nets and Concurrency","author":"\u00c1 Hajdu","year":"2015","unstructured":"Hajdu, \u00c1., V\u00f6r\u00f6s, A., Bartha, T.: New search strategies for the Petri net CEGAR approach. In: Devillers, R., Valmari, A. (eds.) PETRI NETS 2015. LNCS, vol. 9115, pp. 309\u2013328. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-19488-2_16"},{"key":"2_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":"2_CR21","unstructured":"Holt, A.W., Commoner, F.: Events and conditions. In: MAC Conference on Concurrent Systems and Parallel Computation, pp. 3\u201352 (1970)"},{"issue":"1\/2","key":"2_CR22","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)","journal-title":"Formal Methods Syst. Des."},{"issue":"01","key":"2_CR23","first-page":"9","volume":"4","author":"T Kam","year":"1998","unstructured":"Kam, T., Villa, T., Brayton, R.K.: Multi-valued decision diagrams: theory and applications. Multiple-Valued Logic 4(01), 9\u201362 (1998)","journal-title":"Multiple-Valued Logic"},{"issue":"2","key":"2_CR24","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1016\/S0022-0000(69)80011-5","volume":"3","author":"RM Karp","year":"1969","unstructured":"Karp, R.M., Miller, R.E.: Parallel program schemata. J. Comput. Syst. Sci. 3(2), 147\u2013195 (1969)","journal-title":"J. Comput. Syst. Sci."},{"key":"2_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/978-3-662-53401-4_12","volume-title":"Transactions on Petri Nets and Other Models of Concurrency XI","author":"F Kordon","year":"2016","unstructured":"Kordon, F., et al.: MCC\u20192015 \u2013 the fifth model checking contest. In: Koutny, M., Desel, J., Kleijn, J. (eds.) Transactions on Petri Nets and Other Models of Concurrency XI. LNCS, vol. 9930, pp. 262\u2013273. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-53401-4_12"},{"key":"2_CR26","doi-asserted-by":"crossref","unstructured":"Kosaraju, S.R.: Decidability of reachability on vector addition systems. In: ACM Symposium on Theory Computing, pp. 267\u2013281 (1982)","DOI":"10.1145\/800070.802201"},{"key":"2_CR27","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\u2014Getting IT Right","author":"LM Kristensen","year":"2002","unstructured":"Kristensen, L.M., Mailund, T.: A generalised sweep-line method for safety properties. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 549\u2013567. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45614-7_31"},{"key":"2_CR28","unstructured":"Lautenbach, K., Schmid, H.A.: Use of Petri nets for proving correctness of concurrent process systems. In: IFIP Congress, pp. 187\u2013191 (1974)"},{"key":"2_CR29","doi-asserted-by":"crossref","unstructured":"Leroux, J.: The general vector addition system reachability problem by Presburger inductive invariants. In: Proceedings of the LICS, pp. 4\u201313. IEEE (2009)","DOI":"10.1109\/LICS.2009.10"},{"key":"2_CR30","unstructured":"Lipton, R.J.: The reachability problem requires exponential space. Technical report 62, Department of Computer Science, Yale University (1976)"},{"key":"2_CR31","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems - Specification","author":"Z Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems - Specification. Springer, New York (1992). https:\/\/doi.org\/10.1007\/978-1-4612-0931-7"},{"issue":"3","key":"2_CR32","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1137\/0213029","volume":"13","author":"EW Mayr","year":"1984","unstructured":"Mayr, E.W.: An algroithm for the general Petri net reachability problem. SIAM J. Comput. 13(3), 441\u2013460 (1984)","journal-title":"SIAM J. Comput."},{"key":"2_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/3-540-56496-9_14","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"1993","unstructured":"McMillan, K.L.: Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits. In: von Bochmann, G., Probst, D.K. (eds.) CAV 1992. LNCS, vol. 663, pp. 164\u2013177. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/3-540-56496-9_14"},{"key":"2_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/3-540-10001-6_24","volume-title":"Net Theory and Applications","author":"G Memmi","year":"1980","unstructured":"Memmi, G., Roucairol, G.: Linear algebra in net theory. In: Brauer, W. (ed.) Net Theory and Applications. LNCS, vol. 84, pp. 213\u2013223. Springer, Heidelberg (1980). https:\/\/doi.org\/10.1007\/3-540-10001-6_24"},{"key":"2_CR35","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":"2_CR36","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"},{"key":"2_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1007\/3-540-48745-X_3","volume-title":"Application and Theory of Petri Nets 1999","author":"E Pastor","year":"1999","unstructured":"Pastor, E., Cortadella, J., Pe\u00f1a, M.A.: Structural methods to improve the symbolic analysis of Petri nets. In: Donatelli, S., Kleijn, J. (eds.) ICATPN 1999. LNCS, vol. 1639, pp. 26\u201345. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48745-X_3"},{"key":"2_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"416","DOI":"10.1007\/3-540-58152-9_23","volume-title":"Application and Theory of Petri Nets 1994","author":"E Pastor","year":"1994","unstructured":"Pastor, E., Roig, O., Cortadella, J., Badia, R.M.: Petri net analysis using boolean manipulation. In: Valette, R. (ed.) ICATPN 1994. LNCS, vol. 815, pp. 416\u2013435. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-58152-9_23"},{"key":"2_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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 checking using representatives. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 409\u2013423. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/3-540-56922-7_34"},{"key":"2_CR40","unstructured":"Ridder, H.: Analyse von Petri-Netz-Modellen mit Entscheidungsdiagrammen. Ph.D. thesis, Koblenz, Landau, University (1997)"},{"key":"2_CR41","unstructured":"Roch, S., Starke, P.H.: INA: integrated net analyzer (1999)"},{"key":"2_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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 sets for standard properties. In: Donatelli, S., Kleijn, J. (eds.) ICATPN 1999. LNCS, vol. 1639, pp. 46\u201365. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48745-X_4"},{"issue":"7","key":"2_CR43","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 Inf. 36(7), 545\u2013590 (2000)","journal-title":"Acta Inf."},{"key":"2_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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 invariants in state space construction. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 473\u2013488. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-36577-X_35"},{"issue":"3","key":"2_CR45","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/s10009-005-0201-1","volume":"8","author":"K Schmidt","year":"2006","unstructured":"Schmidt, K.: Automated generation of a progress measure for the sweep-line method. STTT 8(3), 195\u2013203 (2006)","journal-title":"STTT"},{"issue":"4\u20135","key":"2_CR46","first-page":"293","volume":"8","author":"PH Starke","year":"1991","unstructured":"Starke, P.H.: Reachability analysis of Petri nets using symmetries. Syst. Anal. Model. Simul. 8(4\u20135), 293\u2013303 (1991)","journal-title":"Syst. Anal. Model. Simul."},{"key":"2_CR47","doi-asserted-by":"crossref","unstructured":"Strehl, K., Thiele, L.: Interval diagram techniques for symbolic model checking of Petri nets. In: Proceedings of the Design, Automation and Test in Europe, pp. 756\u2013757 (1999)","DOI":"10.1145\/307418.307452"},{"issue":"2","key":"2_CR48","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."},{"issue":"2","key":"2_CR49","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1145\/321879.321884","volume":"22","author":"RE Tarjan","year":"1975","unstructured":"Tarjan, R.E.: Efficiency of a good but not linear set union algorithm. J. ACM 22(2), 215\u2013225 (1975)","journal-title":"J. ACM"},{"issue":"1","key":"2_CR50","doi-asserted-by":"publisher","first-page":"1","DOI":"10.3233\/FI-2016-1374","volume":"146","author":"M Triebel","year":"2016","unstructured":"Triebel, M., S\u00fcrmeli, J.: Characterizing stable and deriving valid inequalities of Petri nets. Fundam. Inform. 146(1), 1\u201334 (2016)","journal-title":"Fundam. Inform."},{"key":"2_CR51","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":"2_CR52","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":"2_CR53","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":"2_CR54","unstructured":"Vardi, M.Y.: Verification of concurrent programs: the automata-theoretic framework. In: Proceedings of the LICS, pp. 167\u2013176. IEEE (1987)"},{"key":"2_CR55","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\u201993","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":"2_CR56","doi-asserted-by":"crossref","unstructured":"Wimmel, H., Wolf, K.: Applying CEGAR to the Petri net state equation. Log. Methods Comput. Sci. 8(3) (2012)","DOI":"10.2168\/LMCS-8(3:27)2012"},{"key":"2_CR57","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"},{"key":"2_CR58","unstructured":"Wolf, K.: A simple abstract interpretation for Petri net queries. In: Proceedings of the PNSE, CEUR Workshop Proceedings, vol. 2138, pp. 163\u2013170 (2018)"}],"container-title":["Lecture Notes in Computer Science","Transactions on Petri Nets and Other Models of Concurrency XIV"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-60651-3_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,12,12]],"date-time":"2019-12-12T13:44:00Z","timestamp":1576158240000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-60651-3_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783662606506","9783662606513"],"references-count":58,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-60651-3_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"21 November 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}