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.

翻译：多智能体系统的形式化验证在理论和实践中均具有挑战性。特别是，采用单一验证技术的研究通常效率有限，且仅能验证简单的示例模型。本文提出若干新技术，并将其与近年发展的多种方法相结合，以探究在真实场景中可实现的进展。具体而言，我们运用不动点近似、基于支配的策略搜索、偏序归约及并行化技术，对Selene电子投票协议的可扩展异构模型进行验证。实验结果表明，该组合方法能够验证比先前更为复杂的模型需求。