{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T05:04:56Z","timestamp":1750309496264,"version":"3.41.0"},"reference-count":60,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2025,1,23]],"date-time":"2025-01-23T00:00:00Z","timestamp":1737590400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nd\/4.0\/"}],"funder":[{"name":"JAM"},{"name":"EPSRC Overseas Travel Grant","award":["EP\/V009214\/1"],"award-info":[{"award-number":["EP\/V009214\/1"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2025,1,31]]},"abstract":"<jats:p>\n            We introduce a subclass of concurrent game structures (CGS) with imperfect information in which agents are endowed with private data-sharing capabilities. Importantly, our CGSs are such that it is still decidable to model-check these CGSs against a relevant fragment of ATL. These systems can be thought as a generalization of architectures allowing information forks, that is, cases where strategic abilities lead to certain agents outside a coalition privately sharing information with selected agents inside that coalition. Moreover, in our case, in the initial states of the system, we allow information forks from agents outside a given set\n            <jats:inline-formula content-type=\"math\/tex\">\n              <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\(A\\)<\/jats:tex-math>\n            <\/jats:inline-formula>\n            to agents inside this group\n            <jats:inline-formula content-type=\"math\/tex\">\n              <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\(A\\)<\/jats:tex-math>\n            <\/jats:inline-formula>\n            . For this reason, together with the fact that the communication in our models underpins a specialized form of broadcast, we call our formalism\n            <jats:inline-formula content-type=\"math\/tex\">\n              <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\(A\\)<\/jats:tex-math>\n            <\/jats:inline-formula>\n            <jats:italic>-cast systems<\/jats:italic>\n            . To underline, the fragment of ATL for which we show the model-checking problem to be decidable over\n            <jats:inline-formula content-type=\"math\/tex\">\n              <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\(A\\)<\/jats:tex-math>\n            <\/jats:inline-formula>\n            -cast is a large and significant one; it expresses coalitions over agents in any subset of the set\n            <jats:inline-formula content-type=\"math\/tex\">\n              <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\(A\\)<\/jats:tex-math>\n            <\/jats:inline-formula>\n            . Indeed, as we show, our systems and this ATL fragments can encode security problems that are notoriously hard to express faithfully: terrorist-fraud attacks in identity schemes.\n          <\/jats:p>","DOI":"10.1145\/3704919","type":"journal-article","created":{"date-parts":[[2024,11,19]],"date-time":"2024-11-19T15:49:45Z","timestamp":1732031385000},"page":"1-45","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Model-checking Strategic Abilities in Information-sharing Systems"],"prefix":"10.1145","volume":"26","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7768-1794","authenticated-orcid":false,"given":"Francesco","family":"Belardinelli","sequence":"first","affiliation":[{"name":"Imperial College London, London, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5864-777X","authenticated-orcid":false,"given":"Ioana","family":"Boureanu","sequence":"additional","affiliation":[{"name":"Surrey Centre for Cyber Security, University of Surrey, Guildford, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5981-4533","authenticated-orcid":false,"given":"Catalin","family":"Dima","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Paris-Est Cr\u00e9teil, Creteil, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6138-4229","authenticated-orcid":false,"given":"Vadim","family":"Malvone","sequence":"additional","affiliation":[{"name":"T\u00e9l\u00e9com Paris, Institut Polytechnique de Paris, Paris, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,1,23]]},"reference":[{"key":"e_1_3_2_2_2","unstructured":"European Union. 2016. Regulation (EU) 2016\/679 of the European Parliament and of the Council of 27 April 2016 on the protection of natural persons with regard to the processing of personal data and on the free movement of such data and repealing Directive 95\/46\/EC (General Data Protection Regulation). Official Journal of the European Union L119 (2016) 1\u201388. Retrieved from http:\/\/eur-lex.europa.eu\/legal-content\/EN\/TXT\/?uri=OJ:L:2016:119:TOC"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/3264628"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008739929481"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/585265.585270"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.5555\/3306127.3331930"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.5555\/3091125.3091303"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2020.104552"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394784"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2022.103847"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.251.4"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1613\/jair.1.12539"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2017\/14"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.5555\/3091125.3091301"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2020.103302"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00196726"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.5555\/3091125.3091299"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005136"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10849-009-9115-8"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2016.10.009"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.2001.930138"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28641-4_2"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1109\/MSP.2015.2"},{"key":"e_1_3_2_24_2","series-title":"Lecture Notes in Computer Science","first-page":"344","volume-title":"EUROCRYPT \u201993","author":"Brands S.","year":"1993","unstructured":"S. Brands and D. Chaum. 1993. Distance-Bounding Protocols (Extended Abstract). In EUROCRYPT \u201993, Lecture Notes in Computer Science, Vol. 765, Springer, 344\u2013359."},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/2939918.2939919"},{"key":"e_1_3_2_26_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-642-16242-8_1","volume-title":"Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR \u201910)","volume":"6397","author":"Chatterjee Krishnendu","year":"2010","unstructured":"Krishnendu Chatterjee and Laurent Doyen. 2010. The complexity of partial-observation parity games. In Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR \u201910), Lecture Notes in Computer Science, Vol. 6397, Springer, 1\u201314."},{"key":"e_1_3_2_27_2","volume-title":"Proving Physical Proximity Using Symbolic Models","author":"Debant Alexandre","year":"2018","unstructured":"Alexandre Debant, St\u00e9phanie Delaune, and Cyrille Wiedling. 2018. Proving Physical Proximity Using Symbolic Models. Research Report. Univ Rennes, CNRS, IRISA, France. Retrieved from https:\/\/hal.archives-ouvertes.fr\/hal-01708336"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-29959-0_19"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.25.12"},{"key":"e_1_3_2_30_2","unstructured":"C. Dima and F. L. Tiplea. 2011. Model-checking ATL under imperfect information and perfect recall semantics is undecidable. CoRR abs\/1102.4225 (2011). arXiv:1102.4225. Retrieved from http:\/\/arxiv.org\/abs\/1102.4225"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/5803.001.0001"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-18192-4_12"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.5555\/3545946.3598713"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.53"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/1160633.1160664"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.5555\/3091125.3091292"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1613\/jair.4666"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2016.10.009"},{"key":"e_1_3_2_39_2","first-page":"390","volume-title":"Proceedings of the 15th International Conference on Principles of Knowledge Representation and Reasoning","author":"Gutierrez J.","year":"2016","unstructured":"J. Gutierrez, G. Perelli, and M. Wooldridge. 2016. imperfect information in reactive modules games. In Proceedings of the 15th International Conference on Principles of Knowledge Representation and Reasoning, 390\u2013400. Retrieved from http:\/\/www.aaai.org\/ocs\/index.php\/KR\/KR16\/paper\/view\/12848"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.IC.2018.02.023"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1109\/SECURECOMM.2005.56"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-00419-4_7"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-210049"},{"key":"e_1_3_2_44_2","first-page":"1","article-title":"Agents that know how to play","volume":"62","author":"Jamroga W.","year":"2004","unstructured":"W. Jamroga and W. van der Hoek. 2004. Agents that know how to play. Fund. Inf. 62 (2004), 1\u201335.","journal-title":"Fund. Inf"},{"key":"e_1_3_2_45_2","volume-title":"Introduction to Metamathematics","author":"Kleene S. C.","year":"1952","unstructured":"S. C. Kleene. 1952. Introduction to Metamathematics. North-Holland."},{"key":"e_1_3_2_46_2","first-page":"389","volume-title":"Proceedings 16th Annual IEEE Symposium on Logic in Computer Science","author":"Kupferman O.","year":"2001","unstructured":"O. Kupferman and M. Y. Vardi. 2001. Synthesizing distributed systems. In Proceedings 16th Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society, 389\u2013398."},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-015-0378-x"},{"key":"e_1_3_2_48_2","volume-title":"Ignorance Is Bliss: Observability-Based Dynamic Epistemic Logics and Their Applications","author":"Maffre F.","year":"2016","unstructured":"F. Maffre. 2016. Ignorance Is Bliss: Observability-Based Dynamic Epistemic Logics and Their Applications. Ph.D. Dissertation. Universit\u00e9 Paul Sabatier-Toulouse III."},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2018.00001"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_48"},{"key":"e_1_3_2_51_2","first-page":"562","volume-title":"Proceedings of the International Conference on Concurrency Theory","author":"Meyden R. van der","year":"2005","unstructured":"R. van der Meyden and T. Wilke. 2005. Synthesis of distributed systems from knowledge-based specifications. In Proceedings of the International Conference on Concurrency Theory, 562\u2013576."},{"key":"e_1_3_2_52_2","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-3(3:5)2007"},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75293"},{"issue":"3","key":"e_1_3_2_54_2","article-title":"Algorithms for Omega-regular games with imperfect information","volume":"3","author":"Raskin Jean-Fran\u00e7ois","year":"2007","unstructured":"Jean-Fran\u00e7ois Raskin, Krishnendu Chatterjee, Laurent Doyen, and Thomas A. Henzinger. 2007. Algorithms for Omega-regular games with imperfect information. Log. Methods Comput. Sci. 3, 3 (2007).","journal-title":"Log. Methods Comput. Sci"},{"key":"e_1_3_2_55_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-005-9019-5"},{"key":"e_1_3_2_56_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-50758-3_3"},{"key":"e_1_3_2_57_2","doi-asserted-by":"publisher","DOI":"10.1145\/2970030.2970039"},{"key":"e_1_3_2_58_2","doi-asserted-by":"publisher","DOI":"10.1145\/1160633.1160665"},{"key":"e_1_3_2_59_2","doi-asserted-by":"publisher","DOI":"10.1613\/jair.2901"},{"key":"e_1_3_2_60_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2005.01.003"},{"key":"e_1_3_2_61_2","doi-asserted-by":"publisher","DOI":"10.5555\/1535423"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704919","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704919","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:17:44Z","timestamp":1750295864000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704919"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,23]]},"references-count":60,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2025,1,31]]}},"alternative-id":["10.1145\/3704919"],"URL":"https:\/\/doi.org\/10.1145\/3704919","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2025,1,23]]},"assertion":[{"value":"2024-02-12","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-11","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-23","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}