Questions tagged [mu-calculus]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
0 votes
0 answers
11 views

Is there a CTL* formula that translates into mu-calculus formula 𝜇Y.νZ.(...) with alternation depths 2,1 for Y,Z?

A CTL* formula EFG p is equivalent to mu-calculus formula 𝜇Y.(<>Y | νZ.(<>Z & p)). In this formula, the ...
  • 1,016
1 vote
1 answer
49 views

Generalization of computability to continuous for loops?

A computable function, formulated in the sense of mu recursion, can compute a for or do loop over some (possibly infinite) integer range. I was wondering if a suitable generalization exists that ...
3 votes
0 answers
57 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
3 votes
1 answer
99 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
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 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 votes
1 answer
638 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
1 vote
0 answers
281 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
1 vote
1 answer
109 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
2 answers
837 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
665 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
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
2 votes
1 answer
190 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
1 answer
458 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. \...