Davide Grossi edited untitled.tex  about 8 years ago

Commit id: e43a4025c436b3f3d9797c061db8156d911cf44e

deletions | additions      

       

\end{align}  More precisely, for any influence graph $G = \tuple{\N, R}$, formula $\box{p} \phi \limp \dia{p} \phi$ (respectively, $\dia{p} \phi \limp \box{p} \phi$) is valid in such graph---that is, true in any pointed influence model built on such graph---if and only if $R$ is serial (respectively, functional).\footnote{These are known results from modal correspondence theory (cf. \cite{Blackburn_2001}).}  \subsection{Expressing Convergence}  Eeach stream of opinion profiles $\O^0, \O^1, \ldots, \O^n, \ldots$ corresponds to a stream of influence models $\Model^0, \Model^1, \ldots, \Model^n, \ldots$.   From the point of view of an influence model $\Model = \tuple{\N, \G, \O}$ the BDP dynamics of Definition \ref{def:BDP} can therefore be recast in terms of updates of the valuation function $\O$ as follows:  \begin{itemize}  \item Base: $\O_0 := \O$  \item Step: $\O^{n+1}(p) := \true{\box{p}p}_\Model^n$.  \end{itemize}  That is, the interpretation of $p$ at step $n+1$ is the interpretation of $\box{p}p$ at step $n$.  \begin{fact}  Let $\Model = \tuple{\N, \G, \O}$ be an influence model and $i \in \N$. If pointed $(\Model, i)$ satisfies  \begin{align*}  \nu x. \pm p \land \box{p} x & (p-\Stb)  \end{align*}  then agent $i \in \N$ is stable for $p$.  \end{fact}  \begin{proof}  Assume $\Model, i \models p-\Stb)$. By the semantics of the $\mu$-calculus, formula $\Stb}$ denotes the largest fixpoint of function $\pm p \land \box{p}\cdot$, that is, formula $\box{p^*} \pm p$ where $\box{p^*}$ the modal box interpreted over the reflexive and transitive closure of $R_p$. That is, there exists no $j$ such that $\O_i (p) \neq \O_j(p)$ which is connected by a finite $R_p$ path to $i$. It follows that in the stream generated by the BDP dynamics $i$ cannot change its opinion.  \end{proof}  \begin{proposition}  Let $\Model = \tuple{\N, \G, \O}$ be an influence model. The two following statements are equivalent:  \begin{enumerate}{(i)}  \item $i \in \N$ stabilizes for issue $p \in \Atoms$;  \item $\Model, i \models \mu x. p-\Stb \vee \box{p} x$  \end{enumerate}  \end{proposition}  \begin{proof}  \ldots  \end{proof}  \paragraph{Structural equivalence of BDPs}