Model-checking Strategic Abilities in Information-sharing Systems

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.