论文标题
模型检查信息共享系统中的战略能力
Model Checking Strategic Abilities in Information-sharing Systems
论文作者
论文摘要
我们介绍了一个并发游戏结构（CGS）的子类，并提供不完美的信息，其中代理具有私人数据共享功能。重要的是，我们的CGSs使得与ATL相关片段进行检查这些CGSS仍然可以决定。可以将这些系统视为结构的概括，从某种意义上说，在系统的初始状态下，我们允许从给定代理外的代理商的信息分叉到该A内的代理商A。因此，在模型中的通信基础是广播的专业形式，我们称我们的形式主义a-cast a-cast Systems。为了强调，我们向ATL的片段表明了在A-Cast上可以决定的模型检查问题是一个很大而重要的。它在集合A的任何子集中表达了对代理的联盟。的确，正如我们所显示的，我们的系统和ATL碎片可以编码众所周知，这些问题很难忠实地表达：恐怖分子弗拉德攻击身份方案。
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 generalisation of architectures allowing information forks, in the sense that, in the initial states of the system, we allow information forks from agents outside a given set A to agents inside this A. For this reason, together with the fact that the communication in our models underpins a specialised form of broadcast, we call our formalism A-cast systems. To underline, the fragment of ATL for which we show the model-checking problem to be decidable over A-cast is a large and significant one; it expresses coalitions over agents in any subset of the set A. 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.
