{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,5]],"date-time":"2026-06-05T02:33:30Z","timestamp":1780626810039,"version":"3.54.1"},"reference-count":56,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2017,7,31]],"date-time":"2017-07-31T00:00:00Z","timestamp":1501459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"ERC project EQualIS","award":["FP7-308087"],"award-info":[{"award-number":["FP7-308087"]}]},{"name":"Labex Digicosme, Univ. Paris-Saclay, project VERICONISS"},{"name":"Fonds de recherche du Qu\u00e9bec - Nature et technologies"},{"name":"\u201cChaire Digiteo, ENS Cachan\u2014 \u00c9cole Polytechnique\u201d"},{"DOI":"10.13039\/501100004794","name":"French Centre national de la recherche scientifique","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100004794","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2017,7,31]]},"abstract":"<jats:p>Continuous Petri nets are a relaxation of classical discrete Petri nets in which transitions can be fired a fractional number of times, and consequently places may contain a fractional number of tokens. Such continuous Petri nets are an appealing object to study, since they over-approximate the set of reachable configurations of their discrete counterparts, and their reachability problem is known to be decidable in polynomial time. The starting point of this article is to show that the reachability relation for continuous Petri nets is definable by a sentence of linear size in the existential theory of the rationals with addition and order. Using this characterization, we obtain decidability and complexity results for a number of classical decision problems for continuous Petri nets. In particular, we settle the open problem about the precise complexity of reachability set inclusion. Finally, we show how continuous Petri nets can be incorporated inside the classical backward coverability algorithm for discrete Petri nets as a pruning heuristic to tackle the symbolic state explosion problem. The cornerstone of the approach we present is that our logical characterization enables us to leverage the power of modern SMT-solvers to yield a highly performant and robust decision procedure for coverability in Petri nets. We demonstrate the applicability of our approach on a set of standard benchmarks from the literature.<\/jats:p>","DOI":"10.1145\/3105908","type":"journal-article","created":{"date-parts":[[2017,8,4]],"date-time":"2017-08-04T13:46:14Z","timestamp":1501854374000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":19,"title":["The Logical View on Continuous Petri Nets"],"prefix":"10.1145","volume":"18","author":[{"given":"Michael","family":"Blondin","sequence":"first","affiliation":[{"name":"DIRO, Universit\u00e9 de Montr\u00e9al, Canada, LSV, CNRS 8 ENS Cachan, Universit\u00e9 Paris-Saclay, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alain","family":"Finkel","sequence":"additional","affiliation":[{"name":"LSV, CNRS 8 ENS Cachan, Universit\u00e9 Paris-Saclay, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Christoph","family":"Haase","sequence":"additional","affiliation":[{"name":"LSV, CNRS 8 ENS Cachan, Universit\u00e9 Paris-Saclay, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Serge","family":"Haddad","sequence":"additional","affiliation":[{"name":"LSV, CNRS 8 ENS Cachan, Universit\u00e9 Paris-Saclay 8 INRIA, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2017,8,4]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1996.561359"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02576519"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45319-9_12"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(80)90037-7"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2016.01.011"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_28"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.2307\/2041711"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24288-5_10"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/800113.803630"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2016.06.017"},{"key":"e_1_2_1_11_1","volume-title":"Proceedings of the 8th European Workshop on Application and Theory of Petri Nets. 275--294","author":"David Ren\u00e9","year":"1987","unstructured":"Ren\u00e9 David and Hassane Alla . 1987 . Continuous petri nets . In Proceedings of the 8th European Workshop on Application and Theory of Petri Nets. 275--294 . Ren\u00e9 David and Hassane Alla. 1987. Continuous petri nets. In Proceedings of the 8th European Workshop on Application and Theory of Petri Nets. 275--294."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10669-9"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44585-4_28"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-003-0110-0"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511526558"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38856-9_24"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2414639.2414658"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_40"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008743212620"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-014-0426-0"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80535-8"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00102-X"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/2751290.2751292"},{"key":"e_1_2_1_26_1","unstructured":"Pierre Ganty. 2002. Algorithmes et Structures De Donn\u00e9es Efficaces Pour La Manipulation De Contraintes Sur Les Intervalles (in French). Master\u2019s thesis. Universit\u00e9 Libre de Bruxelles Belgium.  Pierre Ganty. 2002. Algorithmes et Structures De Donn\u00e9es Efficaces Pour La Manipulation De Contraintes Sur Les Intervalles (in French). Master\u2019s thesis. Universit\u00e9 Libre de Bruxelles Belgium."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2005.09.001"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0129054110007180"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-45994-3_6"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/146637.146681"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/SWAT.1974.28"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68894-5_7"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-51963-0_8"},{"key":"e_1_2_1_36_1","unstructured":"Ji Jank. 2009. Issue Tracking Systems. Master\u2019s thesis. Masarykova univerzita Czech Republic.  Ji Jank. 2009. Issue Tracking Systems. Master\u2019s thesis. Masarykova univerzita Czech Republic."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32940-1_35"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2629608"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS.1967.27"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_10"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/800070.802201"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90173-D"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2009.10"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21254-3_3"},{"key":"e_1_2_1_45_1","volume-title":"The Alan Turing Centenary Conference. EasyChair, 214--228","author":"Leroux J\u00e9r\u00f4me","year":"2012","unstructured":"J\u00e9r\u00f4me Leroux . 2012 . Vector addition systems reachability problem (a simpler solution) . In The Alan Turing Centenary Conference. EasyChair, 214--228 . http:\/\/www.easychair.org\/publications\/?page&equals;1673703727 J\u00e9r\u00f4me Leroux. 2012. Vector addition systems reachability problem (a simpler solution). In The Alan Turing Centenary Conference. EasyChair, 214--228. http:\/\/www.easychair.org\/publications\/?page&equals;1673703727"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2015.16"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38856-9_20"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/800076.802477"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(78)90036-1"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48745-X_8"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1016\/0010-4825(95)00042-9"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.5555\/2594845.2594847"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15155-2_54"},{"key":"e_1_2_1_55_1","volume-title":"Theory of Linear and Integer Programming","author":"Schrijver Alexander","unstructured":"Alexander Schrijver . 1998. Theory of Linear and Integer Programming . Wiley . Alexander Schrijver. 1998. Theory of Linear and Integer Programming. Wiley."},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(85)90076-6"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-4437-1"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.5555\/2597902.2597904"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0218126698000043"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/11532231_25"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3105908","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3105908","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:30:04Z","timestamp":1750217404000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3105908"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,7,31]]},"references-count":56,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2017,7,31]]}},"alternative-id":["10.1145\/3105908"],"URL":"https:\/\/doi.org\/10.1145\/3105908","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,7,31]]},"assertion":[{"value":"2016-09-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-05-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-08-04","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}