[Solved]: Intuitive meaning of modal $mu$-calculus formula

Let’s break it down. First, let’s look at $[-a]phi$. This means every non-$a$ transition leads to a state where $phi$ holds. It follows then that $[-a]mathrm{ff}$ holds for states that have no non-$a$ transitions, which we will use when looking at the least fixed point semantics. $langle-ranglemathrm{tt}$ is pretty simple. It holds in any state that has any transition, i.e. is not deadlocked. So together $langle-ranglemathrm{tt} land [-a]phi$ means the state can take a transition and $phi$ holds after every non-$a$ transition. One way to view the meaning of $mu Z.phi(Z)$ is by the approximants referenced in your linked tutorial. If the formula is satisfied in state $s$ then there is some $beta$ such that $bigvee_{alpha<beta} phi^{(alpha)}(mathrm{ff})$ is satisfied in $s$. The notation $phi^{(n)}(x)$ means $phi$ iterated on $x$, $n$ times, i.e. $underbrace{phi(phi(dotsphi(x)))}_{text{$n$ times}}$. Let’s look at some of these. begin{align} phi^{(0)}(mathrm{ff}) &= mathrm{ff} phi^{(1)}(mathrm{ff}) &= langle-ranglemathrm{tt} land [-a]phi^{(0)}(mathrm{ff}) &= langle-ranglemathrm{tt} land [-a]mathrm{ff} phi^{(2)}(mathrm{ff}) &= langle-ranglemathrm{tt} land [-a]phi^{(1)}(mathrm{ff}) &= langle-ranglemathrm{tt} land [-a](langle-ranglemathrm{tt} land [-a]mathrm{ff}) phi^{(3)}(mathrm{ff}) &= langle-ranglemathrm{tt} land [-a]phi^{(2)}(mathrm{ff}) &= langle-ranglemathrm{tt} land [-a](langle-ranglemathrm{tt} land [-a](langle-ranglemathrm{tt} land [-a]mathrm{ff})) end{align} Hopefully it is clear that these have the meanings

1. $phi^{(1)}(mathrm{ff})$: States that can take only $a$ transitions
2. $phi^{(2)}(mathrm{ff})$: Live states that
   1. have only $a$ transitions; or
   2. all length 1 non-$a$ paths lead to a live state with only $a$ transitions
3. $phi^{(3)}(mathrm{ff})$: Live states that
   1. have only $a$ transitions; or
   2. all length 1 non-$a$ paths lead to a live state with only $a$ transitions; or
   3. all length 2 non-$a$ paths lead to a live state with only $a$ transitions

If that is unclear, remember that $[-a]phi$ is trivially satisfied for states with no non-$a$ transitions. Now you should see that $phi^{(n)}(mathrm{ff})$ is true if and only if the state can take at most $n-1$ non-$a$ transitions before reaching a live state with only $a$ transitions. It turns out that $phi^{(n)}(mathrm{ff}) implies phi^{(n+1)}(mathrm{ff})$ so we don’t need to take the disjunction with lesser approximants and can simply say $mu Z. langle-ranglemathrm{tt} land [-a]Z iff exists beta in mathbb{N}. phi^{(beta)}(mathrm{ff})$, or in english, after a finite number of non-$a$ transitions we reach a live state with only $a$ transitions.