{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,25]],"date-time":"2025-06-25T09:25:14Z","timestamp":1750843514449},"reference-count":31,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2014,6,26]],"date-time":"2014-06-26T00:00:00Z","timestamp":1403740800000},"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":["Softw Syst Model"],"published-print":{"date-parts":[[2015,5]]},"DOI":"10.1007\/s10270-014-0422-4","type":"journal-article","created":{"date-parts":[[2014,6,25]],"date-time":"2014-06-25T15:04:45Z","timestamp":1403708685000},"page":"711-717","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["The Petri net twist in explicit model checking"],"prefix":"10.1007","volume":"14","author":[{"given":"Karsten","family":"Wolf","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2014,6,26]]},"reference":[{"key":"422_CR1","doi-asserted-by":"crossref","unstructured":"Bengtsson, J., Larsen, K.G., Larsson, F., Pettersson, P., Wang, Y.: Uppaal\u2013a tool suite for automatic verification of real-time systems. In: Alur, R., Henzinger, T.A., Sontag, E.D. (eds.) Hybrid Systems. Lecture Notes in Computer Science, vol. 1066, pp. 232\u2013243. Springer (1995)","DOI":"10.1007\/BFb0020949"},{"key":"422_CR2","doi-asserted-by":"crossref","unstructured":"Christensen, S., Kristensen, L.M., Mailund, T.: A sweep-line method for state space exploration. In: Margaria, T., Wang, Y. (eds.) TACAS. Lecture Notes in Computer Science, vol. 2031, pp. 450\u2013464. Springer, UK (2001)","DOI":"10.1007\/3-540-45319-9_31"},{"key":"422_CR3","unstructured":"Commoner, F.: Deadlocks in Petri nets. Applied Data Research Inc, Wakefield, Massachusetts, Report CA-7206-2311 (1972)"},{"key":"422_CR4","doi-asserted-by":"crossref","unstructured":"Das, D., Chakrabarti, P.P., Kumar, R.: Functional verification of task partitioning for multiprocessor embedded systems. ACM Trans. Des. Autom. Electron. Syst. 12(4) (2007). doi: 10.1145\/1278349.1278357","DOI":"10.1145\/1278349.1278357"},{"issue":"4","key":"422_CR5","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1007\/s002360050046","volume":"33","author":"J Desel","year":"1996","unstructured":"Desel, J., Reisig, W.: The synthesis problem of Petri nets. Acta Inf. 33(4), 297\u2013315 (1996)","journal-title":"Acta Inf."},{"issue":"3","key":"422_CR6","doi-asserted-by":"crossref","first-page":"277","DOI":"10.1016\/0304-3975(90)90129-6","volume":"70","author":"A Ehrenfeucht","year":"1990","unstructured":"Ehrenfeucht, A., Rozenberg, G.: Theory of 2-structures, part i: clans, basic subclasses, and morphisms. Theor. Comput. Sci. 70(3), 277\u2013303 (1990)","journal-title":"Theor. Comput. Sci."},{"issue":"5","key":"422_CR7","doi-asserted-by":"crossref","first-page":"448","DOI":"10.1016\/j.datak.2011.01.004","volume":"70","author":"D Fahland","year":"2011","unstructured":"Fahland, D., Favre, C., Koehler, J., Lohmann, N., V\u00f6lzer, H., Wolf, K.: Analysis on demand: instantaneous soundness checking of industrial business process models. Data Knowl. Eng. 70(5), 448\u2013466 (2011)","journal-title":"Data Knowl. Eng."},{"key":"422_CR8","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Wolper, P.: Using partial orders for the efficient verification of deadlock freedom and safety properties. In: Larsen, K.G., Skou, A. (eds.) CAV. Lecture Notes in Computer Science, vol. 575, pp. 332\u2013342. Springer (1991)","DOI":"10.1007\/3-540-55179-4_32"},{"key":"422_CR9","unstructured":"Hack, M.H.T.: Analysis of production schemata by Petri nets. Master\u2019s thesis, MIT, Department of Electrical Engineering, Cambridge, Mass (1972)"},{"key":"422_CR10","volume-title":"Unfoldings\u2014A Partial-Order Approach to Model Checking","author":"K Heljanko","year":"2008","unstructured":"Heljanko, K., Esparza, J.: Unfoldings\u2014A Partial-Order Approach to Model Checking. Springer, Berlin (2008)"},{"key":"422_CR11","doi-asserted-by":"crossref","unstructured":"Huber, P., Jensen, A.M., Jepsen, L.O., Jensen, K.: Towards reachability trees for high-level petri nets. In: Rozenberg, G., Genrich, H.J., Roucairol, G. (eds.) European Workshop on Applications and Theory in Petri Nets. Lecture Notes in Computer Science, vol. 188, pp. 215\u2013233. Springer (1984)","DOI":"10.1007\/3-540-15204-0_13"},{"issue":"1\/2","key":"422_CR12","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1007\/BF00625968","volume":"9","author":"C Norris","year":"1996","unstructured":"Norris, C., Dill, D.L.: Better verification through symmetry. Form. Methods Syst. Des. 9(1\/2), 41\u201375 (1996)","journal-title":"Form. Methods Syst. Des."},{"key":"422_CR13","doi-asserted-by":"crossref","unstructured":"Kaiser, A., Kroening, D., Wahl, T.: Dynamic cutoff detection in parameterized concurrent programs. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV. Lecture Notes in Computer Science, vol. 6174, pp. 645\u2013659. Springer (2010)","DOI":"10.1007\/978-3-642-14295-6_55"},{"key":"422_CR14","doi-asserted-by":"crossref","unstructured":"Kordon, F., Linard, A., Buchs, D., Colange, M., Evangelista, S., Lampka, K., Lohmann, N., Paviot-Adet, E., Thierry-Mieg, Y., Wimmel, H.: Report on the model checking contest at Petri nets 2011. T. Petri nets and other models of concurrency 6, 169\u2013196 (2012)","DOI":"10.1007\/978-3-642-35179-2_8"},{"key":"422_CR15","doi-asserted-by":"crossref","unstructured":"Kristensen, L.M., Mailund, T.: A generalised sweep-line method for safety properties. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME. Lecture Notes in Computer Science, vol. 2391, pp. 549\u2013567. Springer (2002)","DOI":"10.1007\/3-540-45614-7_31"},{"issue":"3","key":"422_CR16","doi-asserted-by":"crossref","first-page":"441","DOI":"10.1137\/0213029","volume":"13","author":"EW Mayr","year":"1984","unstructured":"Mayr, E.W.: An algorithm for the general petri net reachability problem. SIAM J. Comput. 13(3), 441\u2013460 (1984)","journal-title":"SIAM J. Comput."},{"key":"422_CR17","doi-asserted-by":"crossref","unstructured":"N\u00fcttgens, M., Feld, T., Zimmermann, V.: Business process modeling with epc and uml: Transformation or integration? pp. 250\u2013261. In: UML, Workshop (1997)","DOI":"10.1007\/978-3-642-48673-9_17"},{"key":"422_CR18","doi-asserted-by":"crossref","unstructured":"Peled, D.: All from one, one for all: on model checking using representatives. In: Courcoubetis, C. (eds.) Computer Aided Verification: Proceedings of 5th International Conference, CAV \u201893 Elounda, Greece, June 28\u2013July 1. LectureNotes in Computer Science, vol. 697. Springer, Berlin, Heidelberg, pp. 409\u2013423","DOI":"10.1007\/3-540-56922-7_34"},{"key":"422_CR19","unstructured":"Petri, C. A.: Kommunikation mit Automaten. In PhD thesis, Technische Universitat Darmstadt, Germany (1962)"},{"issue":"7","key":"422_CR20","doi-asserted-by":"crossref","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":"422_CR21","doi-asserted-by":"crossref","unstructured":"Schmidt, K.: Integrating low level symmetries into reachability analysis. In: Graf, S., Schwartzbach, M.I. (eds.) TACAS. Lecture Notes in Computer Science, vol. 1785, pp. 315\u2013330. Springer (2000)","DOI":"10.1007\/3-540-46419-0_22"},{"key":"422_CR22","unstructured":"Schmidt, K.: Explicit State Space Verification. Humboldt-Universit\u00e4t zu Berlin, Mathematisch-Naturwissenschaftliche Fakult\u00e4t II, Berlin, Germany, Dec, Habilitationsschrift (2002)"},{"issue":"3","key":"422_CR23","doi-asserted-by":"crossref","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"},{"key":"422_CR24","doi-asserted-by":"crossref","unstructured":"Stahl, C., Reisig, W., Krstic, M.: Hazard detection in a GALS wrapper: a case study. In: Desel, J., Watanabe, Y. (eds.) Proceedings of the Fifth International Conference on Application of Concurrency to System Design (ACSD\u201905), pp. 234\u2013243. IEEE Computer Society, St. Malo, France (June 2005)","DOI":"10.1109\/ACSD.2005.20"},{"key":"422_CR25","doi-asserted-by":"crossref","unstructured":"Stern, U., Dill, D.L.: Parallelizing the mur $$\\varphi $$ \u03c6 verifier. In: Grumberg, O. (ed.) CAV, vol. 1254 of Lecture Notes in Computer Science, pp. 256\u2013278. Springer (1997)","DOI":"10.1007\/3-540-63166-6_26"},{"key":"422_CR26","unstructured":"Talcott, C., Dill, D.L.: The pathway logic assistant. In: Third International Workshop on Computational Methods in, Systems Biology, pp. 228\u2013239 (2005)"},{"key":"422_CR27","doi-asserted-by":"crossref","unstructured":"Valmari, A.: Stubborn sets for reduced state space generation. In Rozenberg, G. (ed.) Applications and Theory of Petri Nets, vol. 483 of Lecture Notes in Computer Science, pp. 491\u2013515. Springer (1989)","DOI":"10.1007\/3-540-53863-1_36"},{"key":"422_CR28","doi-asserted-by":"crossref","unstructured":"Valmari, A.: The state explosion problem. In Reisig, W., Rozenberg, G. (eds.) Petri Nets, vol. 1491 of Lecture Notes in Computer Science, pp. 429\u2013528. Springer (1996)","DOI":"10.1007\/3-540-65306-6_21"},{"key":"422_CR29","doi-asserted-by":"crossref","unstructured":"Verbeek, H.M.W., van der Aalst, W.M.P.: Woflan 2.0: A Petri-net-based workflow diagnosis tool. In: ICATPN, pp. 475\u2013484 (2000)","DOI":"10.1007\/3-540-44988-4_28"},{"key":"422_CR30","doi-asserted-by":"crossref","unstructured":"Wolf, K.: Generating Petri net state spaces. In: Kleijn, J., Yakovlev, A. (eds.) ICATPN. Lecture Notes in Computer Science, vol. 4546, pp. 29\u201342. Springer (2007)","DOI":"10.1007\/978-3-540-73094-1_5"},{"key":"422_CR31","doi-asserted-by":"crossref","unstructured":"Wolper, P., Leroy, D.: Reliable hashing without collision detection. In: Courcoubetis, C. (eds.) Computer Aided Verification: Proceedings of 5th International Conference, CAV \u201893 Elounda, Greece, June 28\u2013July 1. LectureNotes in Computer Science, vol. 697. Springer, Berlin, Heidelberg, pp. 59\u201370","DOI":"10.1007\/3-540-56922-7_6"}],"container-title":["Software & Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-014-0422-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10270-014-0422-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-014-0422-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,11]],"date-time":"2019-08-11T22:35:06Z","timestamp":1565562906000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10270-014-0422-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,6,26]]},"references-count":31,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2015,5]]}},"alternative-id":["422"],"URL":"https:\/\/doi.org\/10.1007\/s10270-014-0422-4","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"value":"1619-1366","type":"print"},{"value":"1619-1374","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,6,26]]}}}