Announcements to attentive agents (Q302225)

Given a finite set \(\mathrm{AGT}\) of agents, the language \(\mathcal L\) of \(\mathbf{ABAL}\) \textit{(Attention-Based Announcement Logic)} is built over a countable set \(\mathrm{ATM}\) of propositional variables complemented with propositional variables \(h_a\), \(a\in\mathrm{AGT}\) -- whose intended meaning is ``agent \(a\) is hearing or listening to \dots'' -- using Boolean operators, the modal operators \(B_a\), \(a\in\mathrm{AGT}\) -- whose intended meaning is ``agent \(a\) believes \dots''--, and the modal operators \([\varphi]\), \(\varphi\in\mathcal L\) -- whose intended meaning is ``after public announcement of \(\varphi\), \dots''. Given an \textit{epistemic attention model}, that is, a triple \(M\) of the form \((S,R,V)\) where \(S\) is a nonempty set of states, \(R\) is a mapping from \(\mathrm{AGT}\) into \(S\times S\) (accessibility relation for each agent), and \(V\) is a mapping from \(\mathrm{ATM}\cup\{h_a\mid a\in\mathrm{AGT}\}\) into \(S\) (for the set of states in which a propositional variable is true), and given \(s\in S\), the truth of a formula \(\varphi\) at \((M,s)\), denoted \(M,s\models\varphi\) is inductively defined as follows for the clauses not involving Boolean operators. {\parindent=0.6cm\begin{itemize}\item[--] If \(\varphi\) is a propositional letter \(q\) then \(M,s\models\varphi\) iff \(s\in V(q)\). \item[--] If \(\varphi\) is of the form \(B_a\psi\) then \(M,s\models\varphi\) iff for all \(t\in S\) with \((s,t)\in R_a\), \(M,t\models\psi\). \item[--] If \(\varphi\) is of the form \([\chi]\psi\) then \(M,s\models\varphi\) iff \((S',R',V'),(s,h)\models\psi\) where: {\parindent=0.8cm\begin{itemize}\item[{\(\bullet\)}] \(S'=S\times\{h,\overline{h}\}\) (``heard'' and ``not heard'' copies of \(S\)); \item[{\(\bullet\)}] for \(a\in\mathrm{AGT}\) and \(i,j\in\{h,\overline{h}\}\), \(((s,i),(t,j))\in R'_a\) iff \((s,t)\in R_a\) and: {\parindent=1.0cm \begin{itemize}\item[--] \(i=h\), \(j=h\), \(M,s\models h_a\), and \(M,t\models\chi\), or \item[--] \(i=h\), \(j=\overline{h}\), and \(M,s\not\models h_a\), or \item[--] \(i=\overline{h}\) and \(j=\overline{h}\). \end{itemize}} \end{itemize}} \end{itemize}} The model \(M\) satisfies \textit{attention introspection} iff for all \(a\in\mathrm{AGT}\) and \(s,t\in S\) with \((s,t)\in R_a\), \(s\in V(h_a)\) iff \(t\in V(h_a)\). Setting \(n=|\mathrm{AGT}|\), \(\mathbf{ABAL}\) is shown to be sound and complete for the class of models \({\mathcal K}_n\), and when attention introspection holds, for the class of models \({\mathcal K}45_n^h\), thanks to an axiomatisation whose key axiom is: \[ [\varphi]B_a\psi\leftrightarrow\Bigl(\bigl(h_a\rightarrow B_a(\varphi\rightarrow[\varphi]\psi)\bigr)\wedge(\neg h_a\rightarrow B_a\psi)\Bigr) \] (the belief consequences of an attention-based announcement are either, if the agent pays attention, what the agent believes to be the consequences of the announcement in case it is true, or else, if the agent does not pay attention, what the belief consequences were before the announcement). Thanks to a tableau method, the authors prove that satisfiability of \(\mathcal L\) formulas in the class \({\mathcal K}_n\) of models is \(\mathrm{PSPACE}\)-complete. They then provide a translation of \(\mathbf{ABAL}\) into the action model logic of \textit{A. Baltag}, \textit{L. S. Moss} and \textit{S. Solecki} [``The logic of common knowledge, public announcements, and private suspicions'', in: I. Gilboa (ed.), Proceedings of the 7th conference on theoretical aspects of rationality and knowledge, TARK'98. San Francisco, CA: Morgan Kaufmann Publishers. 43--56 (1998)]. To model attention change, \(\mathcal L\) is extended with modalities of the form \([+A]\) and \([-A]\) where \(A\subseteq\mathrm{AGT}\), to express that all agents in \(A\) pay attention or do not pay attention, respectively, to subsequent announcements. The semantics and both completeness results are adjusted accordingly. This is followed by a few considerations on joint attention, before the last section tackles the issue of common belief, extending \(\mathcal L\) with models operators of the form \(C_A\) and \(\mathbf{C}_A^\varphi\), \(A\subseteq\mathrm{AGT}\), \(\chi\in\mathcal L\), whose intended interpretations are ``agents in \(A\) commonly believe \dots'' and ``relative to \(\chi\), agents in \(A\) commonly believe \dots'', respectively. Completeness results are established, based on two key axioms for common belief after announcement: {\parindent=0.6cm\begin{itemize}\item[--] \([\varphi]\mathbf{C}_A^\chi\psi\leftrightarrow\mathbf{C}_A^{\varphi\wedge[\varphi]\chi}[\varphi]\psi\): the relativised common belief operator only goes through paths where agents are attentive; after announcing \(\varphi\), it goes through all attentive paths satisfying \(\chi\) in the updated models, which are exactly the attentive paths satisfying \(\varphi\wedge[\varphi]\chi\) in the initial model. \item[--] \([\varphi]C_A\psi\leftrightarrow\mathbf{C}^\varphi_A\bigl([\varphi]\psi\wedge\overline{\mathbf{E}}_A(\psi\wedge C_A\psi)\bigr)\wedge\overline{\mathbf{E}}_A(\psi\wedge C_A\psi)\) with \(\overline{\mathbf{E}}_A\chi\) being an abbreviation for \(\bigwedge_{a\in A}(\neg h_a\rightarrow B_a\chi)\): in order for \(A\) to obtain common belief after announcement of \(\varphi\), first inattentive agents in \(A\) should already believe \(\psi\) to be true and to be commonly believed before the announcement, and second, the attentive agents in \(A\) must have common belief of that, and also commonly believe that after the announcement of \(\varphi\), \(\psi\) is true. \end{itemize}}