论文标题
通过申请Three Ballot投票协议来验证战略能力的两次概念
Bisimulations for Verifying Strategic Abilities with an Application to the ThreeBallot Voting Protocol
论文作者
论文摘要
我们提出了在不完美信息下对战略能力进行交替分配的概念。 {\ em Objective}和{\ em主观}的变体具有不完美的信息的{\ em Objective}和{\ em主观}变体的ATL $^*$的公式，这些公式通常用于多代理系统的建模和验证。此外，我们将理论结果应用于对抗强制性抗性的验证，这是一种不使用密码学的投票协议。特别是，我们表明，该协议初始模型的自然简化实际上是原始模型的两次仿真，因此满足了相同的ATL $^*$属性，包括胁迫抗性。这些简化使模型检查工具MCMA与初始模型相比，MCMAS可以终止具有更多选民和候选人的模型。
We propose a notion of alternating bisimulation for strategic abilities under imperfect information. The bisimulation preserves formulas of ATL$^*$ for both the {\em objective} and {\em subjective} variants of the state-based semantics with imperfect information, which are commonly used in the modeling and verification of multi-agent systems. Furthermore, we apply the theoretical result to the verification of coercion-resistance in the ThreeBallot voting system, a voting protocol that does not use cryptography. In particular, we show that natural simplifications of an initial model of the protocol are in fact bisimulations of the original model, and therefore satisfy the same ATL$^*$ properties, including coercion-resistance. These simplifications allow the model-checking tool MCMAS to terminate on models with a larger number of voters and candidates, compared with the initial model.
