deletions | additions       diff --git a/untitled.tex b/untitled.tex  index 6a7110b..9d22714 100644  --- a/untitled.tex  +++ b/untitled.tex 
...
The language of the $\mu$-calculus expands the basic modal language with a least fixpoint operator $\mu$. Here is the BNF of the language:  \[  \L^{\K^{\mu}}: \phi ::= p \mid \bot \mid \neg \phi \mid \phi \land \phi \mid \ldia \dia{p}  \phi \mid \mu p. \phi(p) \]  where $p$ ranges over $\Atoms$ and $\phi(p)$ indicates that $p$ occurs free in $\phi$ (i.e., it is not bounded by fixpoint operators) and under an even number of negations.\footnote{This syntactic restriction guarantees that every formula $\phi(p)$ defines a set transformation which preserves $\subseteq$, which in turn guarantees the existence of least and greatest fixpoints by the Knaster-Tarski fixpoint theorem (cf. \cite{Stirling_2001}).} In general, the notation $\phi(\psi)$ stands for $\psi$ occurs in $\phi$. The usual definitions for Boolean and modal operators apply. Intuitively, $\mu p. \phi(p)$ denotes the smallest formula $p$ such that $p \lequiv \phi(p)$. The greatest fixpoint operator $\nu$ can be defined from $\mu$ as follows: $\nu p. \phi(p) := \neg \mu p. \neg \phi( \neg p)$. 
...
\Model, a \models p \ & \IFF a \in \Val(p), \mbox{ for } p \in {\bf P} \\  \Model, a \models \neg \phi & \IFF a \not\in \true{\phi}_\Model \\  \Model, a \models \phi_1 \wedge \phi_2 & \IFF a \in \true{\phi_1}_\Model \cap \true{\phi_2}_\Model \\  \Model, a \models \ldia \dia{p}  \phi & \IFF a \in \{ b \mid \exists c: b R R_p  c \ \& \ c \in \true{\phi}_\Model \} \\ \Model, a \models \mu p. \phi(p) & \IFF a \in \bigcap \{ X \in 2^A \mid \true{\phi}_{\Model[p:=X]} \subseteq X \}  \end{align*}  where $\true{\phi}_{\Model[p:=X]}$ denotes the truth-set of $\phi$ once $\Val(p)$ is set to be $X$. As usual, we say that: $\phi$ is valid in a model $\M$ iff it is satisfied in all pointed models of $\M$, i.e., $\M \models \phi$; $\phi$ is valid in a class of models iff it is valid in all the model in the class. 
...
\paragraph{Expressing convergence}  \ldots  \paragraph{Validities \paragraph{Structural equivalence  of Influence Graphs}  \ldots BDPs}  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 gives us a natural notion of structural equivalence for BDPs: bisimilar influence graphs give rise to influence processes that behave ìn the same way'.  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%