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.

翻译：本文提出了一种在不完美信息下验证策略能力的交替互模拟概念。该互模拟能保持ATL$^*$公式在基于状态语义的不完美信息下的{\em 客观}与{\em 主观}变体，这两种变体常用于多智能体系统的建模与验证。进一步地，我们将该理论结果应用于三票制投票系统（一种无需密码学的投票协议）的 coercion-resistance 验证中。具体而言，我们证明该协议初始模型的自然简化实际上是原始模型的互模拟，因此满足相同的ATL$^*$性质（包括coercion-resistance）。与原始模型相比，这些简化使得模型检验工具MCMAS能够在包含更多选民和候选人的模型上终止运行。