验证投票的社会技术因素：以2020年波兰邮寄选票为例
摘要：人们设计和实施投票程序，与人合作，并有重要的人为参与。因此，我们应该考虑人为因素，以全面分析选举的属性并检测威胁。特别是，评估参与方的行动和策略（选民、市政办公室员工、邮件职员）如何影响其他参与方行动的结果以及选举的整体结果至关重要。在本文中，我们首次尝试通过波兰2020年总统选举的形式多主体模型来捕捉这些方面。该选举是波兰首次普遍实行邮寄投票。不幸的是，投票方案是在时间压力和政治压力下准备的，未经专家参与。这可能为各种类型的选票欺诈、内部强迫等行为打开了可能性。我们提出了一个初步的可扩展程序模型，形式为多主体图，并通过代理逻辑的公式将选定的完整性和安全性属性进行形式化。然后，我们对模型和公式进行转换，以便将它们作为输入到先进的模型检查器Uppaal中。第一系列实验表明，由于状态空间膨胀，验证效果不佳。然而，我们表明，一种最近发展的可缩减变量抽象的用户友好模型缩减技术使我们能够验证更复杂的情景。
作者：Wojciech Jamroga, Peter Y.A. Ryan, Yan Kim
论文ID：2210.10694
分类：Multiagent Systems
分类简称：cs.MA
提交时间：2022-10-20