deletions | additions       diff --git a/section_Fixpoint_Logics_for_Boolean__.tex b/section_Fixpoint_Logics_for_Boolean__.tex  index decc608..09c2ea5 100644  --- a/section_Fixpoint_Logics_for_Boolean__.tex  +++ b/section_Fixpoint_Logics_for_Boolean__.tex 
...
\fbox{$2) \Rightarrow 1)$} Assume $\Model, i \models \Stb(p)$. By what said above, this implies that there exists no $j$ such that $\O_i (p) \neq \O_j(p)$ which is connected by a finite $G_p$ path to $i$. It follows that in the stream generated by the BDP dynamics $i$ cannot change its opinion, and hence it is stable.  \end{proof}  \begin{theorem} \label{theorem:mu}  Let $\Model = \tuple{\N, \G, \O}$ be an influence model. The two following statements are equivalent:  \begin{enumerate}  \item $i \in \N$ stabilizes for issue $p \in \Atoms$; 
...
\fbox{$1) \Rightarrow 2)$} Assume that $i$ stabilizes for issue $p \in \Atoms$. So there exists a stage $n$ in the stream of profiles generated through Definition \ref{def:BDP} at which $\O_i^n(p) = \O_i^{m}(p)$ for all $m > n$. By Lemma \ref{lemma:stable}, $\tuple{\N, \G, \O^n}, i \models \Stb(p)$. It follows that $i$ is connected through a finite $G_p$-path to an agent $j$ such that $\Model, j \models \Stb(p)$. By what established above we thus have that $\Model, i \models \mu x. \Stb(p) \vee \lbox{p} x$.  \fbox{$2) \Rightarrow 1)$} Assume $\Model, i \models \mu x. \Stb(p) \vee \lbox{p} x$. It follows that $i$ is connected through a finite $G_p$-path to an agent $j$ such that $\Model, j \models \Stb(p)$. By Lemma \ref{lemma:stable} $j$ is therefore stable and therefore $i$ will stabilize for $p$.  \end{proof}  So the formula that expresses the stabilization of the agents' opinions on one issue is $\mu x. \left(\nu y. \pm p \land \lbox{p} y \right) \vee \lbox{p} x$. Informally, the theorem states that in a BDP an agent reaches a stable opinion if and only if it has an indirect influencer (linked by an influence path) whose all direct and indirect influencer have the same opinion.  Notice that such formula has alternation depth $0$. So an off-the-shelf model-checking algorithm for the $\mu$-calculus can check stabilization in time $O(m \cdot n)$ with $n$ being the size of the model and $m$ the size of the formula. It is worth spending a few words on how Now confront  this result relates to Lemmas \ref{lemma:influence} and \ref{lemma:opinion}, as well as with the earlier  Theorem \ref{theorem:convergence}. \ref{theorem:influence}. We have the following corollary:  \begin{corollary}  The BDP for an opinion profile $\O$ based on influence graph $\G$ converges if and only if  \begin{align}  \tuple{\N, \G, \O}, i \models U \left(\bigvee_{p \in \Atoms} \mu x. \Stb(p) \vee \lbox{p} x \right)  \end{align}  for any agent $i \in \N$, where $U$ denotes the universal modality (cf. \cite{Blackburn_2001}).  \end{corollary}  It follows is then not difficult to see  that convergence of a BDPcan be expressed by the following formula  \begin{equation}  U \left(\bigvee_{p \in \Atoms} \mu x. \Stb(p) \vee \lbox{p} x \right)  \end{equation}  and convergence  to a consensus is expressed  by the following one formula of the $\mu$-calculus (with universal modality):  \begin{equation}  \bigvee_{p \in \Atoms} U \left( \mu x. \Stb(p) \vee \lbox{p} x \right).  \end{equation}  where $U$ denotes the universal modality (cf. \cite{Blackburn_2001}).  %\subsection{Structural equivalence of BDPs}