The undecidability of quantified announcements (Q310079)

From MaRDI portal
scientific article
Language Label Description Also known as
English
The undecidability of quantified announcements
scientific article

    Statements

    The undecidability of quantified announcements (English)
    0 references
    7 September 2016
    0 references
    The framework of the paper is expressed in the language of \mathrm{EL}, epistemic logic, consisting of formulas built over a countable set \(P\) of propositional atoms using \(\neg\), \(\wedge\) and the modalities \(K_a\) for \(a\) in a finite set \(A\) of agents, complemented with formulas of the form \([\psi]\varphi\), \([\bullet]\varphi\), \([G]\varphi\) and \([\langle G\rangle]\varphi\) with \(\psi\) an arbitrary formula in the extended language and \(G\) an arbitrary subset of \(A\), giving rise to the logics \mathrm{PAL}\ of \textit{public announcements}, \mathrm{APAL}\ of \textit{arbitrary public announcements}, \mathrm{GAL}\ of \textit{group announcements}, and \mathrm{CAL}\ of \textit{coalition announcements}, respectively. These formulas are interpreted over structures of the form \(M=(S,\sim,V)\) where \(S\) is a nonempty set of worlds, \(\sim\) assigns to each \(a\in A\) an equivalence relation \(\sim_a\) over \(S\) (the world indistinguishability relation for agent \(a\)), and \(V\) assigns to each \(p\in P\) the set of members of \(S\) in which \(p\) in true. Given such a structure \(M\) and \(s\in M\) -- a pair denoted by \(M_s\) --, the notion \(M_s\models\varphi\) is inductively defined as follows. Let \(\mathrm{EL}^G\) be the subset of \mathrm{EL}\ consisting of all formulas of the form \(\bigwedge_{a\in G}K_a\phi_a\), \(a\in G\), \(\phi_a\in\mathrm{EL}\). {\parindent=0.7cm \begin{itemize}\item[--] If \(\varphi\) is of the form \(p\in P\) then \(M_s\models\varphi\) iff \(s\in V(p)\). \item[--] If \(\varphi\) is of the form \(\neg\phi\) then \(M_s\models\varphi\) iff \(M_s\not\models\phi\). \item[--] If \(\varphi\) is of the form \(\phi_1\wedge\phi_2\) then \(M_s\models\varphi\) iff \(M_s\models\phi_1\) and \(M_s\models\phi_2\). \item[--] If \(\varphi\) is of the form \(K_a\phi\) then \(M_s\models\varphi\) iff for all \(t\in S\) with \(s\sim_a t\),\(M_t\models\phi\). \item[--] If \(\varphi\) is of the form \([\psi]\phi\) then \(M_s\models\varphi\) iff \(M_s\models\psi\) implies \(M_s^\psi\models\phi\) where \(M^\psi=(S',\sim',V')\) is such that (1) \(S' =\{s\in S\mid M_s\models\psi\}\), (2) for all \(a\in A\), \(\sim'_a =\sim_a\cap(S'\times S')\) and (3) for all \(p\in P\), \(V'(p)=V(p)\cap S'\): after the true announcement of \(\psi\), \(\phi\) will hold. \item[--] If \(\varphi\) is of the form \([\bullet]\phi\) then \(M_s\models\varphi\) iff for all \(\psi\in\mathrm{EL}\), \(M_s\models[\psi]\phi\): after publicly announcing any true formula of epistemic logic, \(\phi\) is true. \item[--] If \(\varphi\) is of the form \([G]\phi\) then \(M_s\models\varphi\) iff for all \(\psi\in\mathrm{EL}^G\), \(M_s\models[\psi]\phi\): after a group of agents (simultaneously) announce any statement they know to be true, \(\phi\) is true. \item[--] If \(\varphi\) is of the form \([\langle G\rangle]\phi\) then \(M_s\models\varphi\) iff for all \(\psi\in\mathrm{EL}^G\), there exists \(\psi'\in\mathrm{EL}^{A\setminus G}\) with \(M_s\models[\psi\wedge\psi']\phi\): after a group of agents announce any statement they know to be true, and the agents not in the group announce a ``response'' they know to be true, \(\phi\) is true. \end{itemize}} \mathrm{APAL}\ and \mathrm{GAL}\ have been shown to be undecidable, using a construction that requires five agents. In this paper, an improved construction that only requires two agents is presented, providing a complete picture of decidability for these logics as satisfiability for the single agent fragments is trivially decidable. The authors further prove the new result that \mathrm{CAL}\ is also undecidable. The proofs are based on encoding an undecidable tiling problem into the logic.
    0 references
    dynamic epistemic logic
    0 references
    arbitrary public announcements
    0 references
    group announcements
    0 references
    coalition announcements
    0 references
    undecidability results
    0 references
    0 references
    0 references
    0 references
    0 references

    Identifiers