Take the 2-minute tour ×
Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It's 100% free, no registration required.

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

share|improve this question

1 Answer 1

up vote 4 down vote accepted
+50

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.

share|improve this answer

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.