{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T22:34:25Z","timestamp":1784241265869,"version":"3.55.0"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319194875","type":"print"},{"value":"9783319194882","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[[2015]]},"DOI":"10.1007\/978-3-319-19488-2_16","type":"book-chapter","created":{"date-parts":[[2015,6,4]],"date-time":"2015-06-04T05:13:45Z","timestamp":1433394825000},"page":"309-328","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["New Search Strategies for the Petri Net CEGAR Approach"],"prefix":"10.1007","author":[{"given":"\u00c1kos","family":"Hajdu","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andr\u00e1s","family":"V\u00f6r\u00f6s","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Tam\u00e1s","family":"Bartha","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2015,6,4]]},"reference":[{"issue":"5\u20136","key":"16_CR1","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/s10009-007-0044-z","volume":"9","author":"D Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T., Jhala, R., Majumdar, R.: The software model checker Blast. International Journal on Software Tools for Technology Transfer 9(5\u20136), 505\u2013525 (2007)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"16_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/3-540-45319-9_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Ciardo","year":"2001","unstructured":"Ciardo, G., L\u00fcttgen, G., Siminiceanu, R.: Saturation: an efficient iteration strategy for symbolic state-space generation. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 328\u2013342. Springer, Heidelberg (2001)"},{"key":"16_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-3-642-29072-5_3","volume-title":"Transactions on Petri Nets and Other Models of Concurrency v","author":"G Ciardo","year":"2012","unstructured":"Ciardo, G., Zhao, Y., Jin, X.: Ten years of saturation: a Petri net perspective. In: Jensen, K., Donatelli, S., Kleijn, J. (eds.) ToPNoC V. LNCS, vol. 6900, pp. 51\u201395. Springer, Heidelberg (2012)"},{"issue":"5","key":"16_CR4","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E Clarke","year":"2003","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752\u2013794 (2003)","journal-title":"J. ACM"},{"issue":"5","key":"16_CR5","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"EM Clarke","year":"1994","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. 16(5), 1512\u20131542 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"16_CR6","volume-title":"Linear programming 1: introduction","author":"GB Dantzig","year":"1997","unstructured":"Dantzig, G.B., Thapa, M.N.: Linear programming 1: introduction. Springer-Verlag New York Inc., Secaucus (1997)"},{"issue":"2","key":"16_CR7","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/BF00289519","volume":"1","author":"E Dijkstra","year":"1971","unstructured":"Dijkstra, E.: Hierarchical ordering of sequential processes. Acta Informatica 1(2), 115\u2013138 (1971)","journal-title":"Acta Informatica"},{"issue":"3","key":"16_CR8","doi-asserted-by":"crossref","first-page":"401","DOI":"10.14232\/actacyb.21.3.2014.8","volume":"21","author":"\u00c1 Hajdu","year":"2014","unstructured":"Hajdu, \u00c1., V\u00f6r\u00f6s, A., Tam\u00e1s, B., M\u00e1rtonka, Z.: Extensions to the CEGAR approach on Petri nets. Acta Cybernetica 21(3), 401\u2013417 (2014)","journal-title":"Acta Cybernetica"},{"key":"16_CR9","doi-asserted-by":"crossref","unstructured":"John, A., Konnov, I., Schmid, U., Veith, H., Widder, J.: Parameterized model checking of fault-tolerant distributed algorithms by abstraction. In: Formal Methods in Computer-Aided Design (FMCAD), pp. 201\u2013209, October 2013","DOI":"10.1007\/978-3-642-39176-7_14"},{"key":"16_CR10","unstructured":"Kordon, F., Linard, A., Becutti, M., Buchs, D., Fronc, L., Hulin-Hubard, F., Legond-Aubry, F., Lohmann, N., Marechal, A., Paviot-Adet, E., Pommereau, F., Rodr\u00edgues, C., Rohr, C., Thierry-Mieg, Y., Wimmel, H., Wolf, K.: Web report on the model checking contest @ Petri net 2013, June 2013. http:\/\/mcc.lip6.fr"},{"key":"16_CR11","unstructured":"Lipton, R.: The Reachability Problem Requires Exponential Space. Research report, Yale University, Dept. of Computer Science (1976)"},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"Mayr, E.W.: An algorithm for the general Petri net reachability problem. In: Proceedings of the Thirteenth Annual ACM Symposium on Theory of Computing, pp. 238\u2013246. STOC 1981. ACM, New York (1981)","DOI":"10.1145\/800076.802477"},{"issue":"4","key":"16_CR13","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1109\/5.24143","volume":"77","author":"T Murata","year":"1989","unstructured":"Murata, T.: Petri nets: Properties, analysis and applications. Proceedings of the IEEE 77(4), 541\u2013580 (1989)","journal-title":"Proceedings of the IEEE"},{"key":"16_CR14","unstructured":"V\u00f6r\u00f6s, A., Darvas, D., Bartha, T.: Bounded saturation based CTL model checking. In: Proceedings of the 12th Symposium on Programming Languages and Software Tools, SPLST 2011 (2011)"},{"key":"16_CR15","unstructured":"Website of PetriDotNet. http:\/\/inf.mit.bme.hu\/en\/research\/tools\/petridotnet (online accessed March 22, 2015)"},{"key":"16_CR16","unstructured":"Website of the models used in the measurements. http:\/\/inf.mit.bme.hu\/en\/pn2015 (online accessed March 22, 2015)"},{"key":"16_CR17","unstructured":"Website of the SARA tool. http:\/\/www.service-technology.org\/sara\/index.html (online accessed March 22, 2015)"},{"key":"16_CR18","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.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 224\u2013238. Springer, Heidelberg (2011)"},{"key":"16_CR19","doi-asserted-by":"crossref","unstructured":"Wimmel, H., Wolf, K.: Applying CEGAR to the Petri net state equation. Logical Methods in Computer Science 8(3) (2012)","DOI":"10.2168\/LMCS-8(3:27)2012"}],"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-319-19488-2_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,21]],"date-time":"2023-02-21T01:51:26Z","timestamp":1676944286000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-19488-2_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319194875","9783319194882"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-19488-2_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"4 June 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}