Intuitive meaning of modal $\mu$-calculus formula

Question

I am solving one of the past exams and I am not certain with my solution to one of the exercises. The exercise is asking to give intuitive meaning to modal $\mu$-calculus formula:

$$ \phi = \mu Z. \langle - \rangle tt \wedge [-a]Z $$

According to an article Modal logics and mu-calculi: an introduction by Bradfield and Stirling[1] the intuition behind $\mu$ operator is "finite looping". So my reasoning is following: on every path through states in $Z$ there must be only a finite number of transitions with labels different from $a$ and then we must reach a state which is both non-terminal (from the first condition) and all transitions from it are labelled $a$ (from finiteness).

Hence on every path through states in $Z$ there must eventually be a transition labelled $a$. (similar to CTL formula $\forall F(a)$).

Is my reasoning correct? I am unable to find any formal reason for my solution to be right, can you give me a little hint?

[1] http://homepages.inf.ed.ac.uk/jcb/Research/bradfield-stirling-HPA-mu-intro.ps.gz

Answer 1

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-\rangle\mathrm{tt}$ is pretty simple. It holds in any state that has any transition, i.e. is not deadlocked.

So together $\langle-\rangle\mathrm{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(\dots\phi(x)))}_{\text{$n$ times}}$. Let's look at some of these.

\begin{align} \phi^{(0)}(\mathrm{ff}) &= \mathrm{ff} \\ \phi^{(1)}(\mathrm{ff}) &= \langle-\rangle\mathrm{tt} \land [-a]\phi^{(0)}(\mathrm{ff}) \\ &= \langle-\rangle\mathrm{tt} \land [-a]\mathrm{ff} \\ \phi^{(2)}(\mathrm{ff}) &= \langle-\rangle\mathrm{tt} \land [-a]\phi^{(1)}(\mathrm{ff}) \\ &= \langle-\rangle\mathrm{tt} \land [-a](\langle-\rangle\mathrm{tt} \land [-a]\mathrm{ff}) \\ \phi^{(3)}(\mathrm{ff}) &= \langle-\rangle\mathrm{tt} \land [-a]\phi^{(2)}(\mathrm{ff}) \\ &= \langle-\rangle\mathrm{tt} \land [-a](\langle-\rangle\mathrm{tt} \land [-a](\langle-\rangle\mathrm{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-\rangle\mathrm{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.