Verification and Strategy Synthesis for Coalition Announcement Logic

N Alechina; H van Ditmarsch; R Galimullin; T Wang

doi:10.1007/s10849-021-09339-6

Verification and Strategy Synthesis for Coalition Announcement Logic

N Alechina
, H van Ditmarsch
, R Galimullin^*
, T Wang

^*Corresponding author for this work

Research output: Contribution to journal › Article › Academic › peer-review

Abstract

Coalition announcement logic (CAL) is one of the family of the logics of quantified announcements. It allows us to reason about what a coalition of agents can achieve by making announcements in the setting where the anti-coalition may have an announcement of their own to preclude the former from reaching its epistemic goals. In this paper, we describe a PSPACE-complete model checking algorithm for CAL that produces winning strategies for coalitions. The algorithm is implemented in a proof-of-concept model checker.

Original language	English
Pages (from-to)	671-700
Number of pages	30
Journal	Journal of Logic, Language and Information
Volume	30
Issue number	4
DOIs	https://doi.org/10.1007/s10849-021-09339-6
Publication status	Published - Dec 2021

Keywords

Coalition announcement logic
Dynamic epistemic logic
Group announcement logic
Model checking

Access to Document

10.1007/s10849-021-09339-6Licence: CC BY

Cite this

@article{2e339c77f4104f37a7dd7dbbc7fd3925,

title = "Verification and Strategy Synthesis for Coalition Announcement Logic",

abstract = "Coalition announcement logic (CAL) is one of the family of the logics of quantified announcements. It allows us to reason about what a coalition of agents can achieve by making announcements in the setting where the anti-coalition may have an announcement of their own to preclude the former from reaching its epistemic goals. In this paper, we describe a PSPACE-complete model checking algorithm for CAL that produces winning strategies for coalitions. The algorithm is implemented in a proof-of-concept model checker.",

keywords = "Coalition announcement logic, Dynamic epistemic logic, Group announcement logic, Model checking",

author = "N Alechina and \{van Ditmarsch\}, H and R Galimullin and T Wang",

year = "2021",

month = dec,

doi = "10.1007/s10849-021-09339-6",

language = "English",

volume = "30",

pages = "671--700",

journal = "Journal of Logic, Language and Information",

issn = "0925-8531",

publisher = "Springer Science and Business Media B.V.",

number = "4",

}

TY - JOUR

T1 - Verification and Strategy Synthesis for Coalition Announcement Logic

AU - Alechina, N

AU - van Ditmarsch, H

AU - Galimullin, R

AU - Wang, T

PY - 2021/12

Y1 - 2021/12

N2 - Coalition announcement logic (CAL) is one of the family of the logics of quantified announcements. It allows us to reason about what a coalition of agents can achieve by making announcements in the setting where the anti-coalition may have an announcement of their own to preclude the former from reaching its epistemic goals. In this paper, we describe a PSPACE-complete model checking algorithm for CAL that produces winning strategies for coalitions. The algorithm is implemented in a proof-of-concept model checker.

AB - Coalition announcement logic (CAL) is one of the family of the logics of quantified announcements. It allows us to reason about what a coalition of agents can achieve by making announcements in the setting where the anti-coalition may have an announcement of their own to preclude the former from reaching its epistemic goals. In this paper, we describe a PSPACE-complete model checking algorithm for CAL that produces winning strategies for coalitions. The algorithm is implemented in a proof-of-concept model checker.

KW - Coalition announcement logic

KW - Dynamic epistemic logic

KW - Group announcement logic

KW - Model checking

U2 - 10.1007/s10849-021-09339-6

DO - 10.1007/s10849-021-09339-6

M3 - Article

SN - 0925-8531

VL - 30

SP - 671

EP - 700

JO - Journal of Logic, Language and Information

JF - Journal of Logic, Language and Information

IS - 4

ER -

Verification and Strategy Synthesis for Coalition Announcement Logic

Abstract

Keywords

Access to Document

Fingerprint

Cite this