用于验证策略能力的互模拟及其在 ThreeBallot 投票协议中的应用
多智能体系统
2023-10-19 v3
摘要
我们提出了一种针对不完全信息下策略能力的交替互模拟。该互模拟保真了 ATL 公式在基于状态的不完全信息语义的两种常用变体——客观变体与主观变体下的性质，这两种语义常用于多智能体系统的建模与验证。此外，我们将该理论结果应用于不使用密码学的 ThreeBallot 投票系统中共谋抵抗性的验证。特别地，我们展示了该协议初始模型的自然简化实际上是原模型的互模拟，因此满足相同的 ATL 性质，包括共谋抵抗性。与初始模型相比，这些简化使得模型检测工具 MCMAS 能够在具有更多投票人与候选人的模型上终止。
引用
@article{arxiv.2203.13692,
title = {Bisimulations for Verifying Strategic Abilities with an Application to the ThreeBallot Voting Protocol},
author = {Francesco Belardinelli and Rodica Condurache and Catalin Dima and Wojciech Jamroga and Michal Knapik},
journal= {arXiv preprint arXiv:2203.13692},
year = {2023}
}