deletions | additions       diff --git a/section_Fixpoint_Logics_for_Boolean__.tex b/section_Fixpoint_Logics_for_Boolean__.tex  index c6b1970..decc608 100644  --- a/section_Fixpoint_Logics_for_Boolean__.tex  +++ b/section_Fixpoint_Logics_for_Boolean__.tex 
...
\end{align*}  where $\true{\phi}_{\Model[p:=X]}$ denotes the truth-set of $\phi$ once $\O(p)$ is set to be $X$. As usual, we say that: $\phi$ is valid in a model $\Model$ iff it is satisfied in all points of $\Model$, i.e., $\Model \models \phi$; $\phi$ is valid in a class of models iff it is valid in all the models in the class.  \end{definition}  We list some relevant known results about $\K^{\mu}$. The logic has a sound and (weakly) complete axiom system \cite{Walukiewicz_2000}. The satisfiability problem of $\K^{\mu}$ is decidable \cite{Streett_1984}. The complexity of the model-checking problem for $\K^{\mu}$ is known to be in NP $\cap$ co-NP \cite{Gr_del_1999}. It is known that the model-checking problem for a formula of size $m$ and alternation depth $d$ on a system of size $n$ can be solved by the natural fixpoint-approximation algorithm with (time) complexity of $O((m \cdot n)^{d+1})$ \cite{Emerson96}, where the alternation depth of a formula of $\L^\mu$ is the maximum number of $\mu/\nu$ alternations in a chain of nested fixpoint subformulas.\footnote{The reader is referred to, e.g. \cite{Emerson_2001}, for the precise definition.} Finally, the $\mu$-calculus is known to be invariant for bisimulation (cf. \cite{Blackburn_2001}). It actually corresponds to the bisimulation-invariant fragment of monadic second-order logic \cite{Janin_1996}.  \subsection{On the logic of convergence in BDPs} 
...
\end{equation}  where $U$ denotes the universal modality (cf. \cite{Blackburn_2001}).  \subsection{Structural %\subsection{Structural  equivalence of BDPs} The %The  $\mu$-calculus is known to be invariant for bisimulation (cf. \cite{Blackburn_2001}). It actually corresponds to the bisimulation-invariant fragment of monadic second-order logic \cite{Janin_1996}. Therefore bisimulation bisimulati%on  gives us a natural notion of structural equivalence for BDPs: bisimilar influence graphs give rise to influence processes that behave ìn the same way'.