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$^*$公式在状态基语义中常用两种变体（即客观与主观不完全信息版本）下的等价性，这些语义广泛用于多智能体系统的建模与验证。进一步地，我们将该理论结果应用于三票制投票系统（一种无需密码学的投票协议）的抗胁迫性验证中。特别地，我们证明了该协议初始模型的自然简化实际上是原模型的互模拟，因此满足相同的ATL$^*$属性（包括抗胁迫性）。与初始模型相比，这些简化使得模型检测工具MCMAS能够在包含更多选民与候选人的模型上终止运行。