Model-checking strategic abilities in information-sharing systems

DOI10.1145/3704919MaRDI QIDQ7027562zbMATH OpenFDO

Authors Francesco Belardinelli, Ioana Boureanu, Cătălin Dima, Vadim Malvone

Publication date 14 February 2025

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Copyright license Creative Commons Attribution-NoDerivs 4.0 International

Full work available at URL https://doi.org/10.1145/3704919

zbMATH Keywords

alternating-time temporal logicformal specification and verificationlogic and reasoningreasoning about security protocols

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Cites work

• A Hennessy-Milner theorem for ATL with imperfect information
• Algorithms for Omega-Regular Games with Imperfect Information
• Alternating-time temporal logic
• An abstraction-refinement framework for verifying strategic properties in multi-agent systems with imperfect information
• Approximating Perfect Recall when Model Checking Strategic Abilities: Theory and Applications
• Bisimulations for verifying strategic abilities with an application to the ThreeBallot voting protocol
• CONCUR 2005 – Concurrency Theory
• Formal analysis of multiparty contract signing
• From Nondeterministic B\"uchi and Streett Automata to Deterministic Parity Automata
• scientific article; zbMATH DE number 4124989 (Why is no real title available?)
• scientific article; zbMATH DE number 795590 (Why is no real title available?)
• scientific article; zbMATH DE number 1394315 (Why is no real title available?)
• scientific article; zbMATH DE number 7297884 (Why is no real title available?)
• scientific article; zbMATH DE number 7311252 (Why is no real title available?)
• scientific article; zbMATH DE number 3073037 (Why is no real title available?)
• Imperfect information in reactive modules games
• Infinite games with finite knowledge gaps
• Information tracking in games on graphs
• On the logic of cooperation and propositional control
• Reasoning about equilibria in game-like concurrent systems
• Reasoning about the transfer of control
• Relaxing exclusive control in Boolean games
• Security protocol verification: symbolic and computational models
• The Ceteris Paribus Structure of Logics of Game Forms
• The complexity of partial-observation parity games
• Verification of multi-agent systems with public actions against strategy logic

This page was built for publication: Model-checking strategic abilities in information-sharing systems

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