{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T13:47:53Z","timestamp":1742996873612,"version":"3.40.3"},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030992521"},{"type":"electronic","value":"9783030992538"}],"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,29]],"date-time":"2022-03-29T00:00:00Z","timestamp":1648512000000},"content-version":"vor","delay-in-days":87,"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":"Abstract<\/jats:title>Leroux has proved that unreachability in Petri nets can be witnessed by a Presburger separator, i.e. if a marking $$\\boldsymbol{m}_\\text {src}$$<\/jats:tex-math>\n \n \n m<\/mml:mi>\n <\/mml:mrow>\n src<\/mml:mi>\n <\/mml:msub>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula> cannot reach a marking $$\\boldsymbol{m}_\\text {tgt}$$<\/jats:tex-math>\n \n \n m<\/mml:mi>\n <\/mml:mrow>\n tgt<\/mml:mi>\n <\/mml:msub>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula>, then there is a formula $$\\varphi $$<\/jats:tex-math>\n \u03c6<\/mml:mi>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula> of Presburger arithmetic such that: $$\\varphi (\\boldsymbol{m}_\\text {src})$$<\/jats:tex-math>\n \n \u03c6<\/mml:mi>\n (<\/mml:mo>\n \n \n m<\/mml:mi>\n <\/mml:mrow>\n src<\/mml:mi>\n <\/mml:msub>\n )<\/mml:mo>\n <\/mml:mrow>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula> holds; $$\\varphi $$<\/jats:tex-math>\n \u03c6<\/mml:mi>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula> is forward invariant, i.e., $$\\varphi (\\boldsymbol{m})$$<\/jats:tex-math>\n \n \u03c6<\/mml:mi>\n (<\/mml:mo>\n \n m<\/mml:mi>\n <\/mml:mrow>\n )<\/mml:mo>\n <\/mml:mrow>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula> and $$\\boldsymbol{m} \\rightarrow \\boldsymbol{m}'$$<\/jats:tex-math>\n \n \n m<\/mml:mi>\n <\/mml:mrow>\n \u2192<\/mml:mo>\n \n \n m<\/mml:mi>\n <\/mml:mrow>\n \u2032<\/mml:mo>\n <\/mml:msup>\n <\/mml:mrow>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula> imply $$\\varphi (\\boldsymbol{m}'$$<\/jats:tex-math>\n \n \u03c6<\/mml:mi>\n (<\/mml:mo>\n \n \n m<\/mml:mi>\n <\/mml:mrow>\n \u2032<\/mml:mo>\n <\/mml:msup>\n <\/mml:mrow>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula>); and $$\\lnot \\varphi (\\boldsymbol{m}_\\text {tgt})$$<\/jats:tex-math>\n \n \u00ac<\/mml:mo>\n \u03c6<\/mml:mi>\n (<\/mml:mo>\n \n \n m<\/mml:mi>\n <\/mml:mrow>\n tgt<\/mml:mi>\n <\/mml:msub>\n )<\/mml:mo>\n <\/mml:mrow>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula> holds. While these separators could be used as explanations and as formal certificates of unreachability, this has not yet been the case due to their (super-)Ackermannian worst-case size and the (super-)exponential complexity of checking that a formula is a separator. We show that, in continuous Petri nets, these two problems can be overcome. We introduce locally closed separators, and prove that: (a)\u00a0unreachability can be witnessed by a locally closed separator computable in polynomial time; (b)\u00a0checking whether a formula is a locally closed separator is in NC (so, simpler than unreachablity, which is P-complete).<\/jats:p>","DOI":"10.1007\/978-3-030-99253-8_5","type":"book-chapter","created":{"date-parts":[[2022,3,28]],"date-time":"2022-03-28T20:02:48Z","timestamp":1648497768000},"page":"81-100","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Separators in Continuous Petri Nets"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2914-2734","authenticated-orcid":false,"given":"Michael","family":"Blondin","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9862-4919","authenticated-orcid":false,"given":"Javier","family":"Esparza","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,3,29]]},"reference":[{"key":"5_CR1","doi-asserted-by":"publisher","unstructured":"Althaus, E., Beber, B., Kupilas, J., Scholl, C.: Improving interpolants for linear arithmetic. In: Proc. $$\\text{13}^\\text{th }$$ International on Automated Technology for Verification and Analysis (ATVA). pp. 48\u201363 (2015). https:\/\/doi.org\/10.1007\/978-3-319-24953-7_5","DOI":"10.1007\/978-3-319-24953-7_5"},{"key":"5_CR2","doi-asserted-by":"publisher","unstructured":"Baumann, P., Majumdar, R., Thinniyam, R.S., Zetzsche, G.: Context-bounded verification of liveness properties for multithreaded shared-memory programs. Proceedings of the ACM on Programming Languages (PACMPL) 5, 1\u201331 (2021). https:\/\/doi.org\/10.1145\/3434325","DOI":"10.1145\/3434325"},{"key":"5_CR3","doi-asserted-by":"publisher","unstructured":"Beyer, D., Zufferey, D., Majumdar, R.: Csisat: Interpolation for LA+EUF. In: Proc. $$\\text{20 }^\\text{ th }$$ International Conference on Computer Aided Verification (CAV). pp. 304\u2013308 (2008). https:\/\/doi.org\/10.1007\/978-3-540-70545-1_29","DOI":"10.1007\/978-3-540-70545-1_29"},{"key":"5_CR4","doi-asserted-by":"publisher","unstructured":"Blondin, M., Esparza, J., Helfrich, M., Kucera, A., Meyer, P.J.: Checking qualitative liveness properties of replicated systems with stochastic scheduling. In: Proc. $$\\text{32 }^\\text{ nd }$$ International Conference on Computer Aided Verification (CAV). vol. 12225, pp. 372\u2013397 (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_20","DOI":"10.1007\/978-3-030-53291-8_20"},{"key":"5_CR5","doi-asserted-by":"publisher","unstructured":"Blondin, M., Finkel, A., Haase, C., Haddad, S.: The logical view on continuous Petri nets. ACM Transactions on Computational Logic (TOCL) 18(3), 24:1\u201324:28 (2017). https:\/\/doi.org\/10.1145\/3105908","DOI":"10.1145\/3105908"},{"key":"5_CR6","doi-asserted-by":"publisher","unstructured":"Blondin, M., Haase, C.: Logics for continuous reachability in Petri nets and vector addition systems with states. In: Proc. $$\\text{32 }^{nd}$$ Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS). pp. 1\u201312 (2017). https:\/\/doi.org\/10.1109\/LICS.2017.8005068","DOI":"10.1109\/LICS.2017.8005068"},{"key":"5_CR7","unstructured":"Czerwinski, W., Orlikowski, L.: Reachability in vector addition systems is Ackermann-complete. In: Proc. $$\\text{62 }^{nd}$$ Annual IEEE Symposium on Foundations of Computer Science (FOCS) (2021), to appear"},{"key":"5_CR8","doi-asserted-by":"crossref","unstructured":"David, R., Alla, H.: Discrete, Continuous, and Hybrid Petri nets. Springer, 2 edn. (2010)","DOI":"10.1007\/978-3-642-10669-9"},{"key":"5_CR9","doi-asserted-by":"crossref","unstructured":"Desel, J., Esparza, J.: Free choice Petri nets. No.\u00a040, Cambridge University Press (1995)","DOI":"10.1017\/CBO9780511526558"},{"key":"5_CR10","doi-asserted-by":"publisher","unstructured":"Esparza, J., Helfrich, M., Jaax, S., Meyer, P.J.: Peregrine 2.0: Explaining correctness of population protocols through stage graphs. In: Proc. $$\\text{18 }^\\text{ th }$$ International Symposium on Automated Technology for Verification and Analysis (ATVA). vol. 12302, pp. 550\u2013556 (2020). https:\/\/doi.org\/10.1007\/978-3-030-59152-6_32","DOI":"10.1007\/978-3-030-59152-6_32"},{"key":"5_CR11","doi-asserted-by":"publisher","unstructured":"Feng, Y., Martins, R., Wang, Y., Dillig, I., Reps, T.W.: Component-based synthesis for complex APIs. In: Proc. $$\\text{44 }^\\text{ th }$$ ACM SIGPLAN Symposium on Principles of Programming Languages (POPL). pp. 599\u2013612. ACM (2017). https:\/\/doi.org\/10.1145\/3009837.3009851","DOI":"10.1145\/3009837.3009851"},{"key":"5_CR12","doi-asserted-by":"publisher","unstructured":"Fraca, E., Haddad, S.: Complexity analysis of continuous Petri nets. Fundamenta Informaticae 137(1), 1\u201328 (2015). https:\/\/doi.org\/10.3233\/FI-2015-1168","DOI":"10.3233\/FI-2015-1168"},{"key":"5_CR13","doi-asserted-by":"publisher","unstructured":"German, S.M., Sistla, A.P.: Reasoning about systems with many processes. Journal of the ACM 39(3), 675\u2013735 (1992). https:\/\/doi.org\/10.1145\/146637.146681","DOI":"10.1145\/146637.146681"},{"key":"5_CR14","doi-asserted-by":"publisher","unstructured":"Leroux, J.: Vector addition systems reachability problem (A simpler solution). In: Turing-100 \u2013 The Alan Turing Centenary. vol.\u00a010, pp. 214\u2013228 (2012). https:\/\/doi.org\/10.29007\/bnx2","DOI":"10.29007\/bnx2"},{"key":"5_CR15","unstructured":"Leroux, J.: The reachability problem for Petri nets is not primitive recursive. In: Proc. $$\\text{62 }^{nd}$$ Annual IEEE Symposium on Foundations of Computer Science (FOCS) (2021), to appear"},{"key":"5_CR16","doi-asserted-by":"publisher","unstructured":"Leroux, J., Schmitz, S.: Reachability in vector addition systems is primitive-recursive in fixed dimension. In: Proc. $$34^\\text{ th }$$ Symposium on Logic in Computer Science (LICS). pp. 1\u201313 (2019). https:\/\/doi.org\/10.1109\/LICS.2019.8785796","DOI":"10.1109\/LICS.2019.8785796"},{"key":"5_CR17","doi-asserted-by":"publisher","unstructured":"Rybalchenko, A., Sofronie-Stokkermans, V.: Constraint solving for interpolation. Journal of Symbolic Computation 45(11), 1212\u20131233 (2010). https:\/\/doi.org\/10.1016\/j.jsc.2010.06.005","DOI":"10.1016\/j.jsc.2010.06.005"},{"key":"5_CR18","doi-asserted-by":"publisher","unstructured":"Scholl, C., Pigorsch, F., Disch, S., Althaus, E.: Simple interpolants for linear arithmetic. In: Proc. Conference & Exhibition on Design, Automation & Test in Europe (DATE). pp.\u00a01\u20136 (2014). https:\/\/doi.org\/10.7873\/DATE.2014.128","DOI":"10.7873\/DATE.2014.128"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-99253-8_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,3,28]],"date-time":"2022-03-28T20:04:48Z","timestamp":1648497888000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-99253-8_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030992521","9783030992538"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-99253-8_5","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":"29 March 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FoSSaCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","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":"4 April 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2022\/fossacs","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":"77","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":"23","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":"0","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":"30% - 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":"9","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)"}}]}}