{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,5]],"date-time":"2026-10-05T15:43:49Z","timestamp":1791215029060,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642198342","type":"print"},{"value":"9783642198359","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-19835-9_19","type":"book-chapter","created":{"date-parts":[[2011,3,14]],"date-time":"2011-03-14T15:03:16Z","timestamp":1300114996000},"page":"224-238","source":"Crossref","is-referenced-by-count":11,"title":["Applying CEGAR to the Petri Net State Equation"],"prefix":"10.1007","author":[{"given":"Harro","family":"Wimmel","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Karsten","family":"Wolf","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"19_CR1","unstructured":"Berkelaar, M., Eikland, K., Notebaert, P.: lp_solve Reference Guide (2010), \n                    \n                      http:\/\/lpsolve.sourceforge.net\/"},{"issue":"1","key":"19_CR2","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/s10009-005-0188-7","volume":"8","author":"G. Ciardo","year":"2006","unstructured":"Ciardo, G., Marmorstein, R., Siminiceanu, R.: The saturation algorithm for symbolic state space exploration. Software Tools for Technology Transfer\u00a08(1), 4\u201325 (2006)","journal-title":"Software Tools for Technology Transfer"},{"key":"19_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E. Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855. Springer, Heidelberg (2000)"},{"issue":"2","key":"19_CR4","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1023\/A:1008743212620","volume":"16","author":"J. Esparza","year":"2000","unstructured":"Esparza, J., Melzer, S., Sifakis, J.: Verification of safety properties using integer programming: Beyond the state equation. Formal Methods in System Design\u00a016 (2), 159\u2013189 (2000)","journal-title":"Formal Methods in System Design"},{"key":"19_CR5","unstructured":"Garavel, H.: Efficient Petri Net tool for computing quasi-liveness (2003), \n                    \n                      http:\/\/www.informatik.uni-hamburg.de\/cgi-bin\/TGI\/pnml\/getpost?id=2003\/07\/2709"},{"key":"19_CR6","unstructured":"Geeraerts, G., Raskin, J.F., Van Begin, L.: Expand, enlarge and check (2010), \n                    \n                      http:\/\/www.ulb.ac.be\/di\/ssd\/ggeeraer\/eec\/"},{"key":"19_CR7","doi-asserted-by":"crossref","unstructured":"Kosaraju, S.R.: Decidability of reachability in vector addition systems. In: Proceedings of the 14th Annual ACM STOC, pp. 267\u2013281 (1982)","DOI":"10.1145\/800070.802201"},{"issue":"3","key":"19_CR8","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/s10703-006-0006-1","volume":"29","author":"L.M. Kristensen","year":"2006","unstructured":"Kristensen, L.M., 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":"19_CR9","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1016\/0304-3975(92)90173-D","volume":"99","author":"J.L. Lambert","year":"1992","unstructured":"Lambert, J.L.: A structure to decide reachability in Petri nets. Theoretical Computer Science\u00a099, 79\u2013104 (1992)","journal-title":"Theoretical Computer Science"},{"key":"19_CR10","first-page":"4","volume-title":"Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science","author":"J. Leroux","year":"2009","unstructured":"Leroux, J.: The General Vector Addition System Reachability Problem by Presburger Inductive Invariants. In: Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, pp. 4\u201313. IEEE Computer Society, Los Alamitos (2009)"},{"key":"19_CR11","unstructured":"Lipton, R.J.: The Reachability Problem Requires Exponential Space. Research Report\u00a062 (1976)"},{"issue":"3","key":"19_CR12","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1137\/0213029","volume":"13","author":"E. Mayr","year":"1984","unstructured":"Mayr, E.: An algorithm for the general Petri net reachability problem. SIAM Journal of Computing\u00a013(3), 441\u2013460 (1984)","journal-title":"SIAM Journal of Computing"},{"key":"19_CR13","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.\u00a01639, pp. 46\u201365. Springer, Heidelberg (1999)"},{"issue":"3-4","key":"19_CR14","first-page":"325","volume":"47","author":"K. Schmidt","year":"2001","unstructured":"Schmidt, K.: Narrowing petri net state spaces using the state equation. Fundamenta Informaticae\u00a047(3-4), 325\u2013335 (2001)","journal-title":"Fundamenta Informaticae"},{"key":"19_CR15","unstructured":"Talcott, C., Dill, D.: The pathway logic assistent. In: Third International Workshop on Computational Methods in Systems Biology (2005)"},{"key":"19_CR16","unstructured":"Wimmel, H.: Sara \u2013 Structures for Automated Reachability Analysis (2010), \n                    \n                      http:\/\/service-technology.org\/tools\/download"},{"key":"19_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1007\/978-3-540-73094-1_5","volume-title":"Petri Nets and Other Models of Concurrency \u2013 ICATPN 2007","author":"K. Wolf","year":"2007","unstructured":"Wolf, K.: Generating Petri net state spaces. In: Kleijn, J., Yakovlev, A. (eds.) ICATPN 2007. LNCS, vol.\u00a04546, pp. 29\u201342. Springer, Heidelberg (2007)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-19835-9_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,21]],"date-time":"2019-05-21T10:41:54Z","timestamp":1558435314000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-19835-9_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642198342","9783642198359"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-19835-9_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}