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

DOI10.1016/J.IC.2020.104552MaRDI QIDQ2225593zbMATH OpenOpenAlexFDO

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)

Full work available at URL https://arxiv.org/abs/2203.13692, https://home.ipipan.waw.pl/w.jamroga/papers/bisimulation21i+c.pdf

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)

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.

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

Cites work

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

Cited in

(1)

• BISIMULATIONS FOR KNOWING HOW LOGICS

Describes a project that uses

Uses Software

• MCK
• MCMAS
• VerICS

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)