Bisimulations for verifying strategic abilities with an application to the ThreeBallot voting protocol

DOI10.1016/J.IC.2020.104552zbMATH Open1497.68287arXiv2203.13692OpenAlexW3014890138MaRDI QIDQ2225593FDOQ2225593

Authors: Francesco Belardinelli, Rodica Condurache, Wojciech Jamroga, Michał Knapik, Cătălin Dima 

Publication date: 8 February 2021

Published in: Information and Computation (Search for Journal in Brave)

Abstract: We propose a notion of alternating bisimulation for strategic abilities under imperfect information. The bisimulation preserves formulas of ATL${}^{\ast }$ for both the {em objective} and {em subjective} variants of the state-based semantics with imperfect information, which are commonly used in the modeling and verification of multi-agent systems. Furthermore, we apply the theoretical result to the verification of coercion-resistance in the ThreeBallot voting system, a voting protocol that does not use cryptography. In particular, we show that natural simplifications of an initial model of the protocol are in fact bisimulations of the original model, and therefore satisfy the same ATL${}^{\ast }$ properties, including coercion-resistance. These simplifications allow the model-checking tool MCMAS to terminate on models with a larger number of voters and candidates, compared with the initial model.

Full work available at URL: https://arxiv.org/abs/2203.13692

Recommendations

• scientific article; zbMATH DE number 4022620
• Bisimulations and bisimulation games between Verbrugge models
• A Fault Tolerance Bisimulation Proof for Consensus (Extended Abstract)
• Bisimulation, modal logic and model checking games
• scientific article; zbMATH DE number 1361141
• A compositional protocol verification using relativized bisimulation
• scientific article; zbMATH DE number 794261
• Abstracting and Verifying Strategy-Proofness for Auction Mechanisms
• A Complete Axiomatisation of Branching Bisimulation for Probabilistic Systems with an Application in Protocol Verification

zbMATH Keywords

bisimulationsformal verificationalternating-time temporal logicvoting protocols

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Agent technology and artificial intelligence (68T42) Voting theory (91B12) Temporal logic (03B44)

Cites Work

• Modal logic
• Alternating-time temporal logic
• VERICS 2007 -- a model checker for knowledgee and real-time
• Comparing semantics of logics for multi-agent systems
• Title not available (Why is that?)
• A Modal Logic for Coalitional Power in Games
• Communicating sequential processes
• Computer Aided Verification
• Reasoning about strategies
• Reasoning about strategies: on the model-checking problem
• Strategy Logic
• Title not available (Why is that?)
• CSP and anonymity
• Receipt-free secret-ballot elections (extended abstract)
• Title not available (Why is that?)
• Augmenting ATL with strategy contexts
• Model Checking Logics of Strategic Ability: Complexity*
• Practical verification of multi-agent systems against \textsc{Slk} specifications
• Alternating-time logic with imperfect recall
• Reasoning about memoryless strategies under partial observability and unconditional fairness constraints
• Modeling group communication protocols using multiset term rewriting
• The computer ate my vote
• Analysing vote counting algorithms via logic. And its application to the CADE election scheme

Cited In (1)

• BISIMULATIONS FOR KNOWING HOW LOGICS

Uses Software

• VerICS
• MCMAS
• MCK

This page was built for publication: Bisimulations for verifying strategic abilities with an application to the ThreeBallot voting protocol

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2225593)