Voting procedures are designed and implemented by people, for people, and with significant human involvement. Thus, one should take into account the human factors in order to comprehensively analyze properties of an election and detect threats. In particular, it is essential to assess how actions and strategies of the involved agents (voters, municipal office employees, mail clerks) can influence the outcome of other agents' actions as well as the overall outcome of the election. In this paper, we present our first attempt to capture those aspects in a formal multi-agent model of the Polish presidential election 2020. The election marked the first time when postal vote was universally available in Poland. Unfortunately, the voting scheme was prepared under time pressure and political pressure, and without the involvement of experts. This might have opened up possibilities for various kinds of ballot fraud, in-house coercion, etc. We propose a preliminary scalable model of the procedure in the form of a Multi-Agent Graph, and formalize selected integrity and security properties by formulas of agent logics. Then, we transform the models and formulas so that they can be input to the state-of-art model checker Uppaal. The first series of experiments demonstrates that verification scales rather badly due to the state-space explosion. However, we show that a recently developed technique of user-friendly model reduction by variable abstraction allows us to verify more complex scenarios.

翻译：投票程序由人设计、为人实施并涉及大量人员参与。因此，为全面分析选举特性并识别威胁，必须考虑人为因素。尤其需要评估相关参与者（选民、市政工作人员、邮递员）的行为与策略如何影响其他参与者的行动及选举整体结果。本文首次尝试以形式化多智能体模型刻画2020年波兰总统选举中的此类因素。此次选举是波兰首次全面推行邮政投票。遗憾的是，该投票方案在时间与政治压力下仓促制定，且缺乏专家参与，可能导致各类选票欺诈、内部胁迫等风险。我们提出基于多智能体图的初步可扩展程序模型，并通过智能体逻辑公式形式化定义若干完整性与安全属性。随后将模型与公式转化为适用于先进模型检测器Uppaal的输入格式。首轮实验表明，由于状态空间爆炸问题，验证的可扩展性相当有限。然而，我们证明近期提出的基于变量抽象的用户友好型模型化简技术，能够支持对更复杂场景的验证。