Group announcement logic (Q975877): Difference between revisions

The paper studies the differences and relationships between three logics for multi-agent systems; two of them, public announcement logic (PAL) and arbitrary public announcement logic (APAL), come from the literature while the third one, group announcement logic (GAL), is new and is the main topic of the paper. All of them are developed within the framework of epistemic logic for a set \(\{1,\dotsc,n\}\) of agents, using a language \(\mathcal L_{el}\) that contains for each agent \(i\) a modal operator \(K_i\). A Kripke structure \(\mathcal M\) over a set \(S\) of states equips each agent \(i\) with an equivalence relation \(\sim_i\) over \(S\); a formula of the form \(K_i\varphi\) is then true in \(\mathcal M\) at state \(s\), denoted \({\mathcal M},s\models K_i\varphi\), if for all states \(t\) that are \(\sim_i\)-equivalent to \(s\), \({\mathcal M},t\models\varphi\); the intended meaning is that in state \(s\), agent \(i\) knows \(\varphi\). {\parindent5mm \begin{itemize}\item[1)] PAL extends \(\mathcal L_{el}\) with formulas of the form \([\psi]\phi\) with \(\psi\in\mathcal L_{el}\), defined to be true in \(\mathcal M\) at \(s\) just in case if \({\mathcal M},s\models\psi\) then \({\mathcal M}_{|\psi},s\models\phi\), where \({\mathcal M}_{|\psi}\) is the Kripke structure whose states are all \(t\in S\) with \({\mathcal M},t\models\psi\), and that restricts the equivalence relations \(\sim_i\) to this set of states. The dual of \([\psi]\phi\) is denoted \(\langle\psi\rangle\phi\), and \({\mathcal M},s\models\langle\psi\rangle\phi\) intuitively holds if \(\psi\) is true at \(s\) and after \(\psi\) has been announced, \(\phi\) is true at \(s\). \item[2)] APAL extends PAL with formulas of the form \(\square\phi\), defined to be true in \(\mathcal M\) at \(s\) just in case for all \(\psi\in\mathcal L_{el}\), \({\mathcal M},s\models[\psi]\phi\). The dual of \(\square\phi\) is denoted \(\lozenge\phi\), and \({\mathcal M},s\models\lozenge\phi\) intuitively holds if after some formula true at \(s\) has been announced, \(\phi\) is true at \(s\). \item[3)] GAL extends PAL with formulas of the form \([G]\phi\) with \(G\) a set of agents (a subset of \(\{1,\dotsc,n\}\)), defined to be true in \(\mathcal M\) at \(s\) just in case for all sets \(\{\psi_i\mid i\in G\}\) of members of \(\mathcal L_{el}\), \({\mathcal M},s\models[\bigwedge_{i\in G}K_i\psi_i]\phi\). The dual of \([G]\phi\) is denoted \(\langle G\rangle\phi\), and \({\mathcal M},s\models\langle G\rangle\phi\) intuitively holds if after each agent in \(G\) has announced a formula it knows is true at \(s\), all announcements taking place simultaneously, \(\phi\) is true at \(s\). \end{itemize}} The authors give a number of logical properties of GAL, in particular in relation to formulas that involve both a \(K_i\) and the \([G]\) or \(\langle G\rangle\) operators. Most notably, they prove that \({\mathcal M},s\models\langle G\rangle\phi\) is equivalent to \(\phi\) being true in \(\mathcal M\) at \(s\) after a finite sequence of announcements by agents in \(G\) have been made, and they prove a ``Church-Rosser'' property, that is, that a formula of the form \(\langle G\rangle[G]\phi\rightarrow[G]\langle G\rangle\phi\) is valid. They provide a sound and complete axiomatization of GAL, before comparing the expressive power of the three logics, proving that GAL and PAL are equally expressive when \(n=1\) (single agent), that GAL is more expressive than PAL when \(n\geq 2\), and that GAL is not at least as expressive as APAL (the authors conjecture that GAL and APAL are incomparable). They show that the decision problem for GAL is PSPACE-hard. Then the authors discuss some subtleties of GAL around the ability of a coalition to make a formula \(\phi\) come true by making some public announcement (which is what \(\langle G\rangle\phi\) expresses), knowing or not that they -- the members of the coalition -- have this ability, and knowing or not how to do it (what to announce). In the last section, they discuss the relevance of GAL for formalizing security protocols, using the Russian Cards Problem as an example.