Questions tagged [mu-calculus]
The mu-calculus tag has no usage guidance.
12
questions
11
votes
3
answers
3k
views
Why use $\mu$-calculus and not LTL,CTL,CTL*?
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.)
...
- 129
3
votes
1
answer
96
views
Why do we have free variables in mu-calculus?
I'm reading the Model Chekcing book of E. M. Clarke and in the chapter about µ-calculus there is an example formula
$$
f = \mu Z. ((q \mathrel{\mathrm{AND}} Y) \mathrel{\mathrm{OR}} \langle a \rangle ...
- 33
3
votes
0
answers
35
views
CTL and the modal mu-calculus
Is there any literature / results to which fragment of the modal mu-calculus the logic CTL corresponds? I know that in order to tranlsate the until operators of CTL, it suffices to use a single mu-...
- 31
2
votes
1
answer
189
views
Have I got the right understanding of the mu operator?
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 $...
- 217
1
vote
2
answers
1k
views
What does least fix point and greatest fix point mean in Safety games
In safety games there are these mathematical notation about greatest fix points and least fix points but I don't get it. How would we describe them plain English without mathematical symbols.
1
vote
2
answers
826
views
The minimization operator is an effective operator
Assume $\{f_i^{(n)}\}_{i=0}^\infty$ is a Gödel enumeration of the $\mu$-recursive functions of $n$ arguments, such that the $S^m_n$ theorem and the universal function theorem hold. Denote the set of (...
1
vote
1
answer
621
views
Techniques (tools) to convert temporal logic (CTL,CTL* or LTL) to μ-calculus formulae
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 ...
- 129
1
vote
1
answer
447
views
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. \...
- 243
1
vote
1
answer
107
views
Using diagonal argument to prove that $H(x) = \mu y T(x,x,y)$ has no total computable extension
Hello everyone just like the title says I want to prove that $H(x) = \mu y T(x,x,y)$ has no total computable extension such that if we had a function $BIG(x)$ that is both total and agrees with $H(x)$ ...
- 215
1
vote
0
answers
273
views
Using the μ (mu) operator
Problem
I've got this function:
$f(x,y)=(6-3\cdot x)\cdot(y+2)$, with $(x,y)\in\mathbb{N}^2$
Now I have to find $g=\mu f$.
Proposed solution
My solution was to find the smallest $n\in\mathbb{N}$ to ...
- 135
0
votes
1
answer
111
views
Why is $\mu$ finite looping?
It is said that the intuitive meaning of $\mu$ is finite looping where as the intuitive meaning of $\nu$ is infinite looping in $\mu$ calculus. I understand this for finite systems, but why is this ...
- 1,239
-1
votes
1
answer
629
views
Understanding the reason behind the μ (mu) operator [closed]
What is the purpose of the $\mu$ operator?
Is there a real world example?
Is it correct that it can create partial
functions out of total functions and it makes a function $g$ with k
parameters out ...
- 135