Suppose one wants to use a μ-calculus model checker, but specify things in temporal logics, which is easier (more intuitive). Is there a technique (even better, a tool) that automatically translates ...
It is known that the temporal logics LTL,CTL,CTL* can be translated/embedded into the $\mu$-calculus. In other words, the (modal) $\mu$-calculus subsumes these logics, (i.e. it is more expressive.) ...
I have a homework problem that says: For $g(x,y)=xy-5$ compute $h(x) = \mu y(g(x,y))$ and determine its domain. I was under the impression that this means the least y such that $g(x,y)=0$, so then ...
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. ...