Model-checking strategic abilities in information-sharing systems
File(s)
Published version
Author(s)
Belardinelli, Francesco
Boureanu, Ioana
Dima, Catalin
Malvone, Vadim
Type
Journal Article
Abstract
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 퐴 to agents
inside this group 퐴. For this reason, together with the fact that the communication in our models underpins a
specialized form of broadcast, we call our formalism 퐴-cast systems. To underline, the fragment of ATL for
which we show the model-checking problem to be decidable over 퐴-cast is a large and significant one; it
expresses coalitions over agents in any subset of the set 퐴. 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.
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 퐴 to agents
inside this group 퐴. For this reason, together with the fact that the communication in our models underpins a
specialized form of broadcast, we call our formalism 퐴-cast systems. To underline, the fragment of ATL for
which we show the model-checking problem to be decidable over 퐴-cast is a large and significant one; it
expresses coalitions over agents in any subset of the set 퐴. 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.
Date Issued
2025-01-23
Date Acceptance
2024-11-11
Citation
ACM Transactions on Computational Logic, 2025, 26 (1)
ISSN
1529-3785
Publisher
Association for Computing Machinery (ACM)
Journal / Book Title
ACM Transactions on Computational Logic
Volume
26
Issue
1
Copyright Statement
© 2025 Copyright held by the owner/author(s). This work is licensed under Creative Commons Attribution-NoDerivatives International 4.0.
License URL
Identifier
10.1145/3704919
Subjects
CCS Concepts: • Theory of computation Ñ Logic and verification
Verification by model checking
Logic and Reasoning
Alternating-time Temporal Logic
Formal Specification and Verification
Reasoning about Security Protocols
Publication Status
Published
Article Number
5
Date Publish Online
2025-01-23