{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:38:22Z","timestamp":1753889902875,"version":"3.41.2"},"reference-count":1,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2012,9,29]],"date-time":"2012-09-29T00:00:00Z","timestamp":1348876800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We propose a reachability verification technique that combines the Petri net\nstate equation (a linear algebraic overapproximation of the set of reachable\nstates) with the concept of counterexample guided abstraction refinement. In\nessence, we replace the search through the set of reachable states by a search\nthrough the space of solutions of the state equation. We demonstrate the\nexcellent performance of the technique on several real-world examples. The\ntechnique is particularly useful in those cases where the reachability query\nyields a negative result: While state space based techniques need to fully\nexpand the state space in this case, our technique often terminates promptly.\nIn addition, we can derive some diagnostic information in case of\nunreachability while state space methods can only provide witness paths in the\ncase of reachability.<\/jats:p>","DOI":"10.2168\/lmcs-8(3:27)2012","type":"journal-article","created":{"date-parts":[[2013,11,29]],"date-time":"2013-11-29T08:17:46Z","timestamp":1385713066000},"source":"Crossref","is-referenced-by-count":12,"title":["Applying CEGAR to the Petri Net State Equation"],"prefix":"10.46298","volume":"Volume 8, Issue 3","author":[{"given":"Karsten","family":"Wolf","sequence":"first","affiliation":[]},{"given":"Harro","family":"Wimmel","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2012,9,29]]},"reference":[{"key":"684:not-found"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/1036\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/1036\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:01:47Z","timestamp":1681243307000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/1036"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,9,29]]},"references-count":1,"URL":"https:\/\/doi.org\/10.2168\/lmcs-8(3:27)2012","relation":{"is-same-as":[{"id-type":"arxiv","id":"1208.2159","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1208.2159","asserted-by":"subject"}],"is-referenced-by":[{"id-type":"doi","id":"10.1007\/978-3-319-91268-4_18","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2012,9,29]]},"article-number":"1036"}}