{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,25]],"date-time":"2025-06-25T09:26:12Z","timestamp":1750843572160,"version":"3.40.3"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030995232"},{"type":"electronic","value":"9783030995249"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T00:00:00Z","timestamp":1648598400000},"content-version":"vor","delay-in-days":88,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We propose a semi-decision procedure for checking generalized reachability properties, on generalized Petri nets, that is based on the Property Directed Reachability (PDR) method. We actually define three different versions, that vary depending on the method used for abstracting possible witnesses, and that are able to handle problems of increasing difficulty. We have implemented our methods in a model-checker called <jats:sc>SMPT<\/jats:sc> and give empirical evidences that our approach can handle problems that are difficult or impossible to check with current state of the art tools.<\/jats:p>","DOI":"10.1007\/978-3-030-99524-9_28","type":"book-chapter","created":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T06:14:55Z","timestamp":1648534495000},"page":"505-523","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Property Directed Reachability for Generalized Petri Nets"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5969-7346","authenticated-orcid":false,"given":"Nicolas","family":"Amat","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6002-2696","authenticated-orcid":false,"given":"Silvano Dal","family":"Zilio","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5226-8752","authenticated-orcid":false,"given":"Thomas","family":"Hujsa","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,3,30]]},"reference":[{"key":"28_CR1","doi-asserted-by":"publisher","unstructured":"Amat, N., Berthomieu, B., Dal Zilio, S.: On the combination of polyhedral abstraction and SMT-based model checking for Petri nets. In: International Conference on Application and Theory of Petri Nets and Concurrency (Petri Nets). LNCS, vol. 12734. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-76983-3_9","DOI":"10.1007\/978-3-030-76983-3_9"},{"key":"28_CR2","doi-asserted-by":"publisher","unstructured":"Amat, N., Dal\u00a0Zilio, S., Hujsa, T.: SMPT (2022). https:\/\/doi.org\/10.5281\/zenodo.5863379","DOI":"10.5281\/zenodo.5863379"},{"key":"28_CR3","doi-asserted-by":"publisher","unstructured":"Amparore, E., Berthomieu, B., Ciardo, G., Dal\u00a0Zilio, S., Gall\u00e0, F., Hillah, L.M., Hulin-Hubard, F., Jensen, P.G., Jezequel, L., Kordon, F., Le\u00a0Botlan, D., Liebke, T., Meijer, J., Miner, A., Paviot-Adet, E., Srba, J., Thierry-Mieg, Y., van Dijk, T., Wolf, K.: Presentation of the 9th edition of the model checking contest. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Springer (2019). https:\/\/doi.org\/10.1007\/978-3-662-58381-4_9","DOI":"10.1007\/978-3-662-58381-4_9"},{"key":"28_CR4","doi-asserted-by":"publisher","unstructured":"Bardin, S., Finkel, A., Leroux, J., Petrucci, L.: FAST: acceleration from theory to practice. International Journal on Software Tools for Technology Transfer 10(5) (2008). https:\/\/doi.org\/10.1007\/s10009-008-0064-3","DOI":"10.1007\/s10009-008-0064-3"},{"key":"28_CR5","doi-asserted-by":"crossref","unstructured":"Berthomieu, B., Ribet, P.O., Vernadat, F.: The tool TINA\u2013construction of abstract state spaces for Petri nets and time Petri nets. International journal of production research 42(14) (2004)","DOI":"10.1080\/00207540412331312688"},{"key":"28_CR6","doi-asserted-by":"publisher","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic Model Checking without BDDs. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, Springer (1999). https:\/\/doi.org\/10.1007\/3-540-49059-0_14","DOI":"10.1007\/3-540-49059-0_14"},{"key":"28_CR7","doi-asserted-by":"publisher","unstructured":"Blondin, M., Haase, C., Offtermatt, P.: Directed reachability for infinite-state systems. In: Tools and Algorithms for the Construction and Analysis of Systems. LNCS, Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_1","DOI":"10.1007\/978-3-030-72013-1_1"},{"key":"28_CR8","doi-asserted-by":"publisher","unstructured":"Bradley, A.R.: SAT-Based Model Checking without Unrolling. In: Verification, Model Checking, and Abstract Interpretation (VMCAI), LNCS, vol.\u00a06538. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-18275-4_7","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"28_CR9","doi-asserted-by":"publisher","unstructured":"Bradley, A.R.: Understanding IC3. In: Theory and Applications of Satisfiability Testing (SAT), LNCS, vol.\u00a07317. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-31612-8_1","DOI":"10.1007\/978-3-642-31612-8_1"},{"key":"28_CR10","doi-asserted-by":"publisher","unstructured":"Cassez, F., Jensen, P.G., Larsen, K.G.: Refinement of trace abstraction for real-time programs. In: International Workshop on Reachability Problems. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-67089-8_4","DOI":"10.1007\/978-3-319-67089-8_4"},{"key":"28_CR11","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: IC3 modulo theories via implicit predicate abstraction. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_4","DOI":"10.1007\/978-3-642-54862-8_4"},{"key":"28_CR12","doi-asserted-by":"publisher","unstructured":"Czerwi\u0144ski, W., Lasota, S., Lazi\u0107, R., Leroux, J., Mazowiecki, F.: The reachability problem for Petri nets is not elementary. Journal of the ACM (JACM) 68(1) (2020). https:\/\/doi.org\/10.1016\/0304-3975(79)90041-0","DOI":"10.1016\/0304-3975(79)90041-0"},{"key":"28_CR13","unstructured":"Czerwinski, W., Orlikowski, L.: Reachability in vector addition systems is Ackermann-complete. CoRR abs\/2104.13866 (2021), https:\/\/arxiv.org\/abs\/2104.13866"},{"key":"28_CR14","doi-asserted-by":"publisher","unstructured":"David, A., Jacobsen, L., Jacobsen, M., J\u00f8rgensen, K.Y., M\u00f8ller, M.H., Srba, J.: TAPAAL 2.0: Integrated development environment for timed-arc Petri nets. In: Tools and Algorithms for the Construction and Analysis of Systems. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-28756-5_36","DOI":"10.1007\/978-3-642-28756-5_36"},{"key":"28_CR15","doi-asserted-by":"publisher","unstructured":"Dixon, A., Lazi\u0107, R.: Kreach: A tool for reachability in Petri nets. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 12078. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-45190-5_22","DOI":"10.1007\/978-3-030-45190-5_22"},{"key":"28_CR16","doi-asserted-by":"publisher","unstructured":"Esparza, J., Ledesma-Garza, R., Majumdar, R., Meyer, P., Niksic, F.: An SMT-Based Approach to Coverability Analysis. In: Computer Aided Verification (CAV). LNCS (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_40","DOI":"10.1007\/978-3-319-08867-9_40"},{"key":"28_CR17","doi-asserted-by":"publisher","unstructured":"Esparza, J., Melzer, S.: Verification of safety properties using integer programming: Beyond the state equation (2000). https:\/\/doi.org\/10.1023\/A:1008743212620","DOI":"10.1023\/A:1008743212620"},{"key":"28_CR18","doi-asserted-by":"publisher","unstructured":"Finkel, A.: The minimal coverability graph for Petri nets. In: International Conference on Application and Theory of Petri Nets. Springer (1991). https:\/\/doi.org\/10.1007\/3-540-56689-9_45","DOI":"10.1007\/3-540-56689-9_45"},{"key":"28_CR19","doi-asserted-by":"publisher","unstructured":"Finkel, A., Haddad, S., Khmelnitsky, I.: Commodification of accelerations for the Karp and Miller construction. Discret. Event Dyn. Syst. 31(2) (2021). https:\/\/doi.org\/10.1007\/s10626-020-00331-z","DOI":"10.1007\/s10626-020-00331-z"},{"key":"28_CR20","doi-asserted-by":"publisher","unstructured":"Ginsburg, S., Spanier, E.: Semigroups, Presburger formulas, and languages. Pacific journal of Mathematics 16(2) (1966). https:\/\/doi.org\/10.2140\/pjm.1966.16.285","DOI":"10.2140\/pjm.1966.16.285"},{"key":"28_CR21","unstructured":"Hack, M.H.T.: Decidability questions for Petri Nets. Ph.D. thesis, Massachusetts Institute of Technology (1976)"},{"key":"28_CR22","doi-asserted-by":"publisher","unstructured":"Hoder, K., Bj\u00f8rner, N.: Generalized property directed reachability. In: International Conference on Theory and Applications of Satisfiability Testing (SAT). Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-31612-8_13","DOI":"10.1007\/978-3-642-31612-8_13"},{"key":"28_CR23","doi-asserted-by":"publisher","unstructured":"Kang, J., Bai, Y., Jiao, L.: Abstraction-based incremental inductive coverability for Petri nets. In: International Conference on Applications and Theory of Petri Nets and Concurrency. LNCS, vol. 12734. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-76983-3_19","DOI":"10.1007\/978-3-030-76983-3_19"},{"key":"28_CR24","doi-asserted-by":"publisher","unstructured":"Kloos, J., Majumdar, R., Niksic, F., Piskac, R.: Incremental, inductive coverability. In: Computer Aided Verification (CAV). Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_10","DOI":"10.1007\/978-3-642-39799-8_10"},{"key":"28_CR25","doi-asserted-by":"publisher","unstructured":"Kosaraju, S.R.: Decidability of reachability in vector addition systems. In: Proceedings of the Fourteenth Annual ACM Symposium on Theory of Computing. ACM (1982). https:\/\/doi.org\/10.1145\/800070.802201","DOI":"10.1145\/800070.802201"},{"key":"28_CR26","doi-asserted-by":"publisher","unstructured":"Leroux, J.: The general vector addition system reachability problem by Presburger inductive invariants. In: 2009 24th Annual IEEE Symposium on Logic In Computer Science. IEEE (2009). https:\/\/doi.org\/10.1109\/LICS.2009.10","DOI":"10.1109\/LICS.2009.10"},{"key":"28_CR27","doi-asserted-by":"publisher","unstructured":"Murata, T.: State equation, controllability, and maximal matchings of petri nets. IEEE Transactions on Automatic Control 22(3) (1977). https:\/\/doi.org\/10.1109\/TAC.1977.1101509","DOI":"10.1109\/TAC.1977.1101509"},{"key":"28_CR28","doi-asserted-by":"publisher","unstructured":"Sheeran, M., Singh, S., St\u00e5lmarck, G.: Checking Safety Properties Using Induction and a SAT-Solver. In: Formal Methods in Computer-Aided Design. LNCS, Springer, Berlin, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-40922-X_8","DOI":"10.1007\/3-540-40922-X_8"},{"key":"28_CR29","doi-asserted-by":"publisher","unstructured":"Silva, M., Terue, E., Colom, J.M.: Linear algebraic and linear programming techniques for the analysis of place\/transition net systems. In: Advanced Course on Petri Nets. Springer (1998). https:\/\/doi.org\/10.1007\/3-540-65306-6_19","DOI":"10.1007\/3-540-65306-6_19"},{"key":"28_CR30","doi-asserted-by":"publisher","unstructured":"Thierry-Mieg, Y.: Symbolic Model-Checking Using ITS-Tools. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Springer (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_20","DOI":"10.1007\/978-3-662-46681-0_20"},{"key":"28_CR31","doi-asserted-by":"publisher","unstructured":"Thierry-Mieg, Y.: Structural reductions revisited. In: Application and Theory of Petri Nets and Concurrency. LNCS, vol. 12152. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-51831-8_15","DOI":"10.1007\/978-3-030-51831-8_15"},{"key":"28_CR32","unstructured":"Wimmel, H.: Sara: Structures for automated reachability analysis (2013), https:\/\/github.com\/nlohmann\/service-technology.org\/tree\/master\/sara"},{"key":"28_CR33","doi-asserted-by":"publisher","unstructured":"Wimmel, H., Wolf, K.: Applying CEGAR to the Petri net state equation. Logical Methods in Computer Science 8 (2012). https:\/\/doi.org\/10.2168\/LMCS-8(3:27)2012","DOI":"10.2168\/LMCS-8(3:27)2012"},{"key":"28_CR34","doi-asserted-by":"publisher","unstructured":"Wolf, K.: Petri net model checking with LoLA 2. In: Application and Theory of Petri Nets and Concurrency. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-91268-4_18","DOI":"10.1007\/978-3-319-91268-4_18"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-99524-9_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T06:26:52Z","timestamp":1648535212000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-99524-9_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030995232","9783030995249"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-99524-9_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"30 March 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Munich","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 April 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 April 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2022\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"159","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"46","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"29% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"10","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"16 tool papers of the affiliated competition SV-Comp and 1 paper consisting of the competition report are also included in the proceedings","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}