Verification of Multi-Agent Properties in Electronic Voting: A Case Study
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2023
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866912195055452160 |
|---|---|
| author | Kurpiewski, Damian Jamroga, Wojciech Maśko, Łukasz Mikulski, Łukasz Pazderski, Witold Penczek, Wojciech Sidoruk, Teofil |
| author_facet | Kurpiewski, Damian Jamroga, Wojciech Maśko, Łukasz Mikulski, Łukasz Pazderski, Witold Penczek, Wojciech Sidoruk, Teofil |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2310_15789 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Verification of Multi-Agent Properties in Electronic Voting: A Case Study Kurpiewski, Damian Jamroga, Wojciech Maśko, Łukasz Mikulski, Łukasz Pazderski, Witold Penczek, Wojciech Sidoruk, Teofil Multiagent Systems 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. |
| title | Verification of Multi-Agent Properties in Electronic Voting: A Case Study |
| topic | Multiagent Systems |
| url | https://arxiv.org/abs/2310.15789 |