I've been reading up on modal $\mu$-calculus via this paper "The mu-calculus and model-checking" to get a better intuition for fixed-point logic.
In the paper, the authors state that the formula $\mu X .\langle a\rangle X$ "is just false" but I don't really understand why. From what I see, $\mu X .\langle a\rangle X$ could mean that "there is a finite sequence of $a$-transitions".
Can you please point out, what I am missing? Thanks for any help!
Perhaps the easiest way to see this is using the approximation approach outlined on page 5: $$\mu^0X.\langle a \rangle X = \emptyset$$ $$\mu^1X.\langle a \rangle X = \langle a \rangle \emptyset = \emptyset,$$ so we have already reached a fixpoint, and hence $\left[\!\left[ \mu X.\langle a \rangle X \right]\!\right] = \emptyset$. In other words, the formula holds in no states, which is what is meant by a formula being false.