# Intuitive meaning of modal $\mu$-calculus formula

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

-

## 1 Answer

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.

-
{"extraction_info": {"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 51, "mathjax_display_tex": 1, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0}, "config": {"markdown_headings": true, "markdown_code": true, "boilerplate_config": {"ratio_threshold": 0.18, "absolute_threshold": 10, "end_threshold": 15, "enable": true}, "remove_buttons": true, "remove_image_figures": true, "remove_link_clusters": true, "table_config": {"min_rows": 2, "min_cols": 3, "format": "github"}, "remove_chinese": true, "remove_edit_buttons": true, "extract_latex": true}, "english_confidence": 0.8835461139678955, "perplexity_flag": "middle"}