{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,22]],"date-time":"2025-08-22T22:10:03Z","timestamp":1755900603834,"version":"3.44.0"},"reference-count":27,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2024,5,10]],"date-time":"2024-05-10T00:00:00Z","timestamp":1715299200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100006374","name":"HORIZON EUROPE Framework Programme","doi-asserted-by":"publisher","award":["GA n. 101135513 (CyclOps)"],"award-info":[{"award-number":["GA n. 101135513 (CyclOps)"]}],"id":[{"id":"10.13039\/501100006374","id-type":"DOI","asserted-by":"publisher"}]},{"name":"PRIN MUR","award":["Prot. 2020FNEB27 (PINPOINT)"],"award-info":[{"award-number":["Prot. 2020FNEB27 (PINPOINT)"]}]},{"DOI":"10.13039\/501100008815","name":"Free University of Bozen-Bolzano","doi-asserted-by":"crossref","award":["ADAPTERS project"],"award-info":[{"award-number":["ADAPTERS project"]}],"id":[{"id":"10.13039\/501100008815","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100004063","name":"Knut and Alice Wallenberg Foundation","doi-asserted-by":"crossref","award":["WASP Program"],"award-info":[{"award-number":["WASP Program"]}],"id":[{"id":"10.13039\/501100004063","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100015273","name":"Province of Bolzano","doi-asserted-by":"crossref","award":["DFG grant n. 500249124 (D2G2)"],"award-info":[{"award-number":["DFG grant n. 500249124 (D2G2)"]}],"id":[{"id":"10.13039\/501100015273","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Proc. ACM Manag. Data"],"published-print":{"date-parts":[[2024,5,10]]},"abstract":"<jats:p>We study verification of reachability properties over Communicating Datalog Programs (CDPs), which are networks of relational nodes connected through unordered channels and running Datalog-like computations. Each node manipulates a local state database (DB), depending on incoming messages and additional input DBs from external services. Decidability of verification for CDPs has so far been established only under boundedness assumptions on the state and channel sizes, showing at the same time undecidability of reachability for unbounded states with only two unary relations or unbounded channels with a single binary relation. The goal of this paper is to study the open case of CDPs with bounded states and unbounded channels, under the assumption that channels carry unary relations only. We discuss the significance of the resulting model and prove the decidability of verification of variants of reachability, captured in fragments of first-order CTL. We do so through a novel reduction to coverability problems in a class of high-level Petri Nets that manipulate unordered data identifiers. We study the tightness of our results, showing that minor generalizations of the considered reachability properties yield undecidability of verification, both for CDPs and the corresponding Petri Net model.<\/jats:p>","DOI":"10.1145\/3651590","type":"journal-article","created":{"date-parts":[[2024,5,14]],"date-time":"2024-05-14T08:32:13Z","timestamp":1715675533000},"page":"1-26","source":"Crossref","is-referenced-by-count":0,"title":["Verification of Unary Communicating Datalog Programs"],"prefix":"10.1145","volume":"2","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4878-7581","authenticated-orcid":false,"given":"C.","family":"Aiswarya","sequence":"first","affiliation":[{"name":"Chennai Mathematical Institute, Siruseri, India"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5174-9693","authenticated-orcid":false,"given":"Diego","family":"Calvanese","sequence":"additional","affiliation":[{"name":"Free University of Bozen-Bolzano &amp; Ume\u00e5 University, Bolzano, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5692-5681","authenticated-orcid":false,"given":"Francesco","family":"Di Cosmo","sequence":"additional","affiliation":[{"name":"Free University Bozen-Bolzano, Bolzano, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8021-3430","authenticated-orcid":false,"given":"Marco","family":"Montali","sequence":"additional","affiliation":[{"name":"Free University of Bozen-Bolzano, Bolzano, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,5,14]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2463676.2465251"},{"key":"e_1_2_1_2_1","unstructured":"Peter Alvaro Tom J. Ameloot Joseph M. Hellerstein William Marczak and Jan Van den Bussche. 2011. A Declarative Semantics for Dedalus. Technical Report UCB\/EECS-2011--120. EECS Department University of California Berkeley. http:\/\/www.eecs.berkeley.edu\/Pubs\/TechRpts\/2011\/EECS-2011--120.html"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2014.01.005"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2463664.2465221"},{"key":"e_1_2_1_5_1","volume-title":"Proc. of the 14th Int. Conf. on Principles of Knowledge Representation and Reasoning (KR). AAAI Press, 458--467","author":"Hariri Babak Bagheri","year":"2014","unstructured":"Babak Bagheri Hariri, Diego Calvanese, Marco Montali, and Alin Deutsch. 2014. State-Boundedness in Data-Aware Dynamic Systems. In Proc. of the 14th Int. Conf. on Principles of Knowledge Representation and Reasoning (KR). AAAI Press, 458--467."},{"volume-title":"Principles of Model Checking","author":"Baier Christel","key":"e_1_2_1_6_1","unstructured":"Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking. The MIT Press."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25535-9_10"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.18452\/9417"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2463664.2467796"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2017.08.007"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2022\/354"},{"key":"e_1_2_1_12_1","volume-title":"Proc. of the 36th Italian Conf. on Computational Logic (CILC 2021) (CEUR Workshop Proceedings","volume":"76","author":"Calvanese Diego","year":"2021","unstructured":"Diego Calvanese, Francesco Di Cosmo, Jorge Lobo, and Marco Montali. 2021. Convergence Verification of Declarative Distributed Systems. In Proc. of the 36th Italian Conf. on Computational Logic (CILC 2021) (CEUR Workshop Proceedings, Vol. 3002). CEUR-WS.org, 62--76."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2016.04.006"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3212019.3212025"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2006.10.006"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1142351.1142364"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.is.2022.102011"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1860702.1860704"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(69)80011-5"},{"key":"e_1_2_1_20_1","first-page":"251","article-title":"Nets with Tokens which Carry Data","volume":"88","author":"Lazic Ranko","year":"2008","unstructured":"Ranko Lazic, Thomas Christopher Newcomb, Jo\u00ebl Ouaknine, A. W. Roscoe, and James Worrell. 2008. Nets with Tokens which Carry Data. Fundamenta Informaticae, Vol. 88, 3 (2008), 251--274.","journal-title":"Fundamenta Informaticae"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/TKDE.2016.2515604"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/1095587"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2017.02.002"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2011.05.007"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-45005-1_18"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1514894.1514896"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02424-5_18"}],"container-title":["Proceedings of the ACM on Management of Data"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3651590","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3651590","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,22]],"date-time":"2025-08-22T21:40:56Z","timestamp":1755898856000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3651590"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,5,10]]},"references-count":27,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2024,5,10]]}},"alternative-id":["10.1145\/3651590"],"URL":"https:\/\/doi.org\/10.1145\/3651590","relation":{},"ISSN":["2836-6573"],"issn-type":[{"type":"electronic","value":"2836-6573"}],"subject":[],"published":{"date-parts":[[2024,5,10]]}}}