Verification of Multi-Agent Properties in Electronic Voting: A Case Study
Damian Kurpiewski, Wojciech Jamroga, Łukasz Maśko, Łukasz Mikulski, Witold Pazderski, Wojciech Penczek, Teofil Sidoruk
TL;DR
The paper tackles the hard problem of verifying strategic-epistemic properties in realistic multi-agent systems by integrating multiple verification techniques, including fixpoint approximation, depth-first strategy search, domination-based pruning, and partial-order reduction, with parallelized variants. It extends POR to handle nested epistemic modalities within subjective strategic ability and applies the approach to a modular, scalable model of the Selene e-voting protocol. The results demonstrate verification of more sophisticated Selene models than prior work and provide insights into the relative strengths of each technique, showing practical gains from parallelization and POR while identifying limitations of some approaches. The work offers a concrete methodology and technical contributions that advance scalable MAS verification for socio-technical systems and points toward broader applicability to real-world protocols.
Abstract
Formal verification of multi-agent systems is hard, both theoretically and in practice. In particular, studies that use a single verification technique typically show limited efficiency, and allow to verify only toy examples. Here, we propose some new techniques and combine them with several recently developed ones to see what progress can be achieved for a real-life scenario. Namely, we use fixpoint approximation, domination-based strategy search, partial order reduction, and parallelization to verify heterogeneous scalable models of the Selene e-voting protocol. The experimental results show that the combination allows to verify requirements for much more sophisticated models than previously.