Bisimulations for verifying strategic abilities with an application to the ThreeBallot voting protocol
Bisimulations for verifying strategic abilities with an application to the ThreeBallot voting protocol
复制标题
通过应用 ThreeBallot 投票协议来验证战略能力的双向模拟
DOI：
10.1016/j.ic.2020.104552
复制
发表时间：
2021
影响因子：
1
通讯作者：
Belardinelli F
中科院分区：
文献类型：
--
作者：
Belardinelli F
本文提出了不完全信息下战略能力的交替互模拟概念。互模拟保持ATL的公式为基于状态的语义的{\em客观}和{\em主观}变体与不完美的信息，这是常用的多智能体系统的建模和验证。此外，我们将理论结果应用于三票制投票系统（一种不使用密码学的投票协议）中的抗干扰性验证。特别是，我们表明，协议的初始模型的自然简化实际上是原始模型的互模拟，因此满足相同的ATL属性，包括抗干扰性。这些简化允许模型检查工具MCMAS终止于与初始模型相比具有更大数量的选民和候选人的模型。
We propose a notion of alternating bisimulation for strategic abilities under imperfect information. The bisimulation preserves formulas of ATLfor 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 ATLproperties, 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.
登录
查看更多内容
DOI：
--
发表时间：
2016
期刊：
Adaptive Agents and Multi-Agent Systems
影响因子：
--
作者：
W. Jamroga;M. Knapik;Damian Kurpiewski
通讯作者：
Damian Kurpiewski
游戏的三值抽象：不确定性，但精确
DOI：
--
发表时间：
2004
期刊：
Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, 2004.
影响因子：
--
作者：
L. D. Alfaro;Patrice Godefroid;R. Jagadeesan
通讯作者：
R. Jagadeesan
验证投票协议
DOI：
--
发表时间：
2013
期刊：
International Conference on Interactive Theorem Proving
影响因子：
--
作者：
C. Schürmann
通讯作者：
C. Schürmann
电脑吃了我的选票
DOI：
--
发表时间：
2010
期刊：
影响因子：
--
作者：
P. Ryan
通讯作者：
P. Ryan
验证投票方案
影响因子：
5.6
作者：
Bernhard Beckert;R. Goré;C. Schürmann;Thorsten Bormer;Jian Wang
通讯作者：
Jian Wang