Modal mu-calculus

Definition

Let $P$ be a set of propositions, $A$ a set of actions and $\mathcal{V}$ a set of variables. The formulas of the modal $\mu$-calculus are given by the grammar $$\varphi ::= p \mid Z \mid \neg\varphi \mid \varphi \land \varphi \mid \langle a \rangle \varphi \mid \mu Z.\,\varphi, \qquad p \in P,\ a \in A,\ Z \in \mathcal{V}.$$ In a formula $\mu Z.\,\varphi$, every free occurrence of $Z$ in $\varphi$ must lie under an even number of negations.

A model is a labelled transition system $\mathcal{M} = (S, \set{\xrightarrow{a}}_{a \in A}, V)$ with a valuation $V \colon P \to \mathcal{P}(S)$. Given an assignment $\rho \colon \mathcal{V} \to \mathcal{P}(S)$, the set $\|\varphi\|_\rho \subseteq S$ is defined by induction:

1. $\|p\|_\rho = V(p)$ and $\|Z\|_\rho = \rho(Z)$;
2. $\|\neg\varphi\|_\rho = S \setminus \|\varphi\|_\rho$ and $\|\varphi \land \psi\|_\rho = \|\varphi\|_\rho \cap \|\psi\|_\rho$;
3. $\|\langle a \rangle \varphi\|_\rho = \set{s \in S : s \xrightarrow{a} t \text{ for some } t \in \|\varphi\|_\rho}$;
4. $\|\mu Z.\,\varphi\|_\rho = \bigcap \set{T \subseteq S : \|\varphi\|_{\rho[Z \mapsto T]} \subseteq T}$.

Here $\rho[Z \mapsto T]$ agrees with $\rho$ except that it sends $Z$ to $T$.