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

DOI10.1016/j.ic.2020.104552zbMath1497.68287arXiv2203.13692OpenAlexW3014890138MaRDI QIDQ2225593

Michał Knapik, Wojciech Jamroga, Rodica Condurache, Francesco Belardinelli, Catalin 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

zbMATH Keywords

formal verificationbisimulationsalternating-time temporal logicvoting protocols

Mathematics Subject Classification ID

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

Related Items

BISIMULATIONS FOR KNOWING HOW LOGICS

Uses Software

• VerICS
• MCMAS
• MCK

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Augmenting ATL with strategy contexts
• Practical verification of multi-agent systems against \textsc{Slk} specifications
• Reasoning about memoryless strategies under partial observability and unconditional fairness constraints
• Comparing semantics of logics for multi-agent systems
• Receipt-free secret-ballot elections (extended abstract)
• Reasoning About Strategies
• Model Checking Logics of Strategic Ability: Complexity*
• Alternating-time temporal logic
• Strategy Logic
• The Computer Ate My Vote
• Communicating sequential processes
• A Modal Logic for Coalitional Power in Games
• Analysing Vote Counting Algorithms via Logic
• CSP and anonymity
• Computer Aided Verification