Bisimulations for verifying strategic abilities with an application to the ThreeBallot voting protocol
OA Location
Author(s)
Belardinelli, Francesco
Condurache, Rodica
Dima, Catalin
Jamroga, Wojciech
Knapik, Michal
Type
Journal Article
Abstract
We propose a notion of alternating bisimulation for strategic abilities under imperfect information. The bisimulation preserves formulas of ATL⁎ for both the objective and 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⁎ 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.
Date Issued
2021-02
Date Acceptance
2019-06-11
Citation
Information and Computation, 2021, 276
ISSN
0890-5401
Publisher
Elsevier
Journal / Book Title
Information and Computation
Volume
276
Copyright Statement
© 2020 Elsevier Inc. All rights reserved.
Identifier
https://www.webofscience.com/api/gateway?GWVersion=2&SrcApp=PARTNER_APP&SrcAuth=LinksAMR&KeyUT=WOS:000607516300007&DestLinkType=FullRecord&DestApp=ALL_WOS&UsrCustomerID=a2bf6146997ec60c407a63945d4e92bb
Subjects
Alternating-time Temporal Logic
ANONYMITY
Bisimulations
Computer Science
Computer Science, Theory & Methods
Formal verification
LOGIC
Mathematics
Mathematics, Applied
MODEL CHECKING
Physical Sciences
Science & Technology
SYSTEMS
Technology
UNCERTAINTY
VERIFICATION
Voting protocols
Publication Status
Published
Article Number
104552
Date Publish Online
2020-03-30