用于验证策略能力的互模拟及其在三票制投票协议中的应用
Bisimulations for Verifying Strategic Abilities with an Application to the ThreeBallot Voting Protocol
AI总结：
本文提出不完全信息下策略能力的交替互模拟，保持ATL$^*$公式，应用于无密码三票制投票协议的强制抵抗性验证，简化模型使MCMAS可处理更多选民与候选人。
摘要：
我们提出了一种在不完全信息下针对策略能力的交替互模拟概念。该互模拟保持了ATL$^*$公式在基于状态语义的不完全信息下的客观和主观变体，这些变体常用于多智能体系统的建模与验证。此外，我们将这一理论结果应用于三票制投票系统（一种不使用密码学的投票协议）中强制抵抗性的验证。特别地，我们表明对协议初始模型的自然简化实际上是原始模型的互模拟，因此满足相同的ATL$^*$属性，包括强制抵抗性。这些简化使得模型检测工具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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
