deletions | additions       diff --git a/section_Fixpoint_Logics_for_Boolean__.tex b/section_Fixpoint_Logics_for_Boolean__.tex  index 536e1bc..7f2ff6b 100644  --- a/section_Fixpoint_Logics_for_Boolean__.tex  +++ b/section_Fixpoint_Logics_for_Boolean__.tex 
...
\end{itemize}  That is, the interpretation of $p$ at step $n+1$ is the interpretation of $\lbox{p}p$ at step $n$. Equivalently, the interpretation of $\neg p$ at step $n+1$ is the interpretation of $\lbox{p}\neg p$ at step $n$.  \begin{fact} \label{fact:stable} \begin{lemma} \label{lemma:stable}  Let $\Model = \tuple{\N, \G, \O}$ be an influence model and $i \in \N$. If pointed $(\Model, i)$ satisfies  \begin{align*}  \Stb(p) := \nu x. \pm p \land \lbox{p} x   \end{align*}  then agent $i \in \N$ is stable for $p$.\footnote{Notice that $\pm p$ is used as a variable ranging over $\set{p, \neg p}$. Technically the above formula is to be read as a scheme for $\nu x. p \land \lbox{p} x$ and $\nu x. \pm \neg p \land \lbox{p} x$.}  \end{fact} \end{lemma}  \begin{proof}  Assume $\Model, i \models \Stb(p)$. By the semantics of the $\mu$-calculus, formula $\Stb(p)$ denotes the largest fixpoint of function $\pm p \land \lbox{p}(\cdot)$, that is, formula $\lbox{p^*} \pm p$ where $\lbox{p^*}$ is 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} 
...
\end{enumerate}  \end{theorem}  \begin{proof}  \fbox{$1) \Rightarrow 2)$} Assume that $i$ stabilizes for issue $p \in \Atoms$.   \fbox{$2) \Rightarrow 1)$} Assume $\Model, i \models \mu x. \Stb(p) \vee \lbox{p} x$. By First of all observe that, by  the semantics of the $\mu$-calculus $i$ belongs to $\mu x. \Stb(p) \vee \lbox{p} x$ denotes  the smallest fixpoint of equation $\pm p $x  \lequiv \Stb(p) \vee \lbox{p} \pm p$. x$.  By the Knaster-Tarski theorem and the fact that influence models are finite, we can compute such fixpoint as $\bigcup_{0 \leq n < \omega} \true{\Stb(p)^n}$ where $\true{\Stb(p)^0} = \true{\true{\Stb(p) \vee \lbox{p} \bot}$ (notice that $\lbox{p} \bot \lequiv \bot$ on influence models) and $\true{\Stb(p)^{n+1}} = \true{\Stb(p) \vee \lbox{p}\Stb(p)^n}$. Rephrasing this fixpoint approximation So,  by \ref{fact:stable} that means, Lemma \ref{lemma:stable} $i$ belongs to $\true{\mu x. \Stb(p) \vee \lbox{p} x}$  either $i$ is stable for issue $p$ or has access in a finite number of steps to a an agent who is stable for $p$. \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$ will is connected through a finite $R_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 $R_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$. 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.