{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,17]],"date-time":"2026-04-17T13:02:52Z","timestamp":1776430972041,"version":"3.51.2"},"reference-count":23,"publisher":"Association for Computing Machinery (ACM)","issue":"2","funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"crossref","award":["EP\/T022124\/1"],"award-info":[{"award-number":["EP\/T022124\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/100014013","name":"UKRI","doi-asserted-by":"crossref","award":["I4035"],"award-info":[{"award-number":["I4035"]}],"id":[{"id":"10.13039\/100014013","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":[[2026,4,30]]},"abstract":"<jats:p>We present results concerning the expressiveness and decidability of a popular graph learning formalism, graph neural networks (GNNs), exploiting connections with logic. We use a family of recently-discovered decidable logics involving \u201cPresburger quantifiers.\u201d We show how to use these logics to measure the expressiveness of classes of GNNs, in some cases getting exact correspondences between the expressiveness of logics and GNNs. We also employ the logics, and the techniques used to analyze them, to obtain decision procedures for verification problems over GNNs. We complement this with undecidability results for static analysis problems involving the logics, as well as for GNN verification problems.<\/jats:p>","DOI":"10.1145\/3800944","type":"journal-article","created":{"date-parts":[[2026,3,10]],"date-time":"2026-03-10T14:11:26Z","timestamp":1773151886000},"page":"1-65","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Decidability of Graph Neural Networks via Logical Characterizations"],"prefix":"10.1145","volume":"27","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2964-0880","authenticated-orcid":false,"given":"Michael","family":"Benedikt","sequence":"first","affiliation":[{"name":"Oxford University, Oxford, United Kingdom of Great Britain and Northern Ireland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-5446-9150","authenticated-orcid":false,"given":"Chia-Hsuan","family":"Lu","sequence":"additional","affiliation":[{"name":"Oxford University, Oxford, United Kingdom of Great Britain and Northern Ireland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-8341-2004","authenticated-orcid":false,"given":"Tony","family":"Tan","sequence":"additional","affiliation":[{"name":"University of Liverpool, Liverpool, United Kingdom of Great Britain and Northern Ireland"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2026,4,17]]},"reference":[{"key":"e_1_3_2_2_1","volume-title":"ICLR","author":"Barcel\u00f3 Pablo","year":"2020","unstructured":"Pablo Barcel\u00f3, Egor V. Kostylev, Mika\u00ebl Monet, Jorge P\u00e9rez, Juan L. Reutter, and Juan Pablo Silva. 2020. The logical expressiveness of graph neural networks. In ICLR."},{"key":"e_1_3_2_3_1","unstructured":"Pablo Barcel\u00f3 Alexander Kozachinskiy Anthony Wijdada Lin and Vladamir Podolskii. 2023. Logical languages accepted by transformer encoders with hard attention. Retrieved from https:\/\/arxiv.org\/abs\/2310.03817"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.52202\/079017-0175"},{"key":"e_1_3_2_5_1","volume-title":"FSTTCS","author":"Bednarczyk Bartosz","year":"2021","unstructured":"Bartosz Bednarczyk, Maja Orlowska, Anna Pacanowska, and Tony Tan. 2021. On classical decidable logics extended with percentage quantifiers and arithmetics. In FSTTCS."},{"key":"e_1_3_2_6_1","volume-title":"ICALP","author":"Benedikt Michael","year":"2024","unstructured":"Michael Benedikt, Chia-Hsuan Lu, Boris Motik, and Tony Tan. 2024. Decidability of graph neural networks via logical characterizations. In ICALP."},{"key":"e_1_3_2_7_1","first-page":"1","volume-title":"ICML","author":"Chiang David","year":"2023","unstructured":"David Chiang, Peter Cholak, and Anand Pillay. 2023. Tighter bounds on the expressivity of transformer encoders. In ICML, 1\u201319."},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.orl.2005.09.008"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1570-2464(07)80008-5"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470677"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS56636.2023.10175735"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785850"},{"key":"e_1_3_2_13_1","volume-title":"CAV","author":"Katz Guy","year":"2017","unstructured":"Guy Katz, Clark W. Barrett, David L. Dill, Kyle Julian, and Mykel J. Kochenderfer. 2017. Reluplex: An efficient SMT solver for verifying deep neural networks. In CAV."},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/11532231_20"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1137\/0206033"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-20(3:16)2024"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/164759"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/1095587"},{"key":"e_1_3_2_19_1","volume-title":"IJCAI","author":"Nunn Pierre","year":"2024","unstructured":"Pierre Nunn, Marco S\u00e4lzer, Fran\u00e7ois Schwarzentruber, and Nicolas Troquard. 2024. A logic for reasoning about aggregate-combine graph neural networks. In IJCAI."},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/322276.322287"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-89716-1_10"},{"key":"e_1_3_2_22_1","volume-title":"ICLR","author":"S\u00e4lzer Marco","year":"2023","unstructured":"Marco S\u00e4lzer and Martin Lange. 2023. Fundamental limits in formal verification of message-passing neural networks. In ICLR."},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(70)80006-X"},{"key":"e_1_3_2_24_1","volume-title":"ICLR","author":"Xu Keyulu","year":"2019","unstructured":"Keyulu Xu, Weihua Hu, Jure Leskovec, and Stefanie Jegelka. 2019. How powerful are graph neural networks. In ICLR."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3800944","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,17]],"date-time":"2026-04-17T12:24:57Z","timestamp":1776428697000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3800944"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,4,17]]},"references-count":23,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2026,4,30]]}},"alternative-id":["10.1145\/3800944"],"URL":"https:\/\/doi.org\/10.1145\/3800944","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,4,17]]},"assertion":[{"value":"2025-01-22","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-02-17","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-04-17","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}