Talk:Modal μ-calculus

Requested move

Modal μ calculus → Modal mu calculus — By WP:ENGLISH, pages names should use the Latin alphabet only. eboy 09:34, 11 October 2006 (UTC)

Survey

Add  * '''Support'''  or  * '''Oppose'''  on a new line followed by a brief explanation, then sign your opinion using ~~~~.

• Comment I think there are bigger problems with the article name, and with the article's very existence, than that issue. Isn't it already covered somewhere else? Is this terminology in commen enough use anywhere in the real world that a redirect from it to somewhere else would be useful? Or is this just something made up for a Wikipedia article name? Gene Nygaard 02:28, 20 October 2006 (UTC)

  There's mu operator article; this one should probably be a redirect with a merger (if we have that LTL logic explained somewhere). Duja 12:27, 23 October 2006 (UTC)

  Maybe it is better to name the article mu calculus, i.e. to leave out the word modal. In either case, this logic (or family of logics) certainly deserves a page on its own: a lot of research (both theory and applications) has been done on this subject, and it is certainly an established name in the field of computer science. Also, a Google search for mu calculus gives me almost a 100.000 hits. eboy 15:36, 23 October 2006 (UTC)

• I agree, it is a better name mu-calculus alone, but this article requires to expand and maybe include the dual nu-calculus (maximal fixed points)

in that case the article may call fixed points, and the mu calculus an nu calculus articles redirect to the page including both subjects.

Discussion

Add any additional comments:

I merged this to mu operator, as a substub not really worth a separate article. This mathematic area seems a bit esoteric (it's Greek to me I admit), so we'd better leave this to the experts. Duja 09:05, 24 October 2006 (UTC)

em... I don't want to call myself an expert on the mu calculus, although I am developing one right now. The fact that it seems esoteric, is because it is not a simple calculus. However, because something is not simple doesn't mean that it shouldn't be on Wikipedia. To put it even stronger:

• any book on model checking treats the mu-calculus;
• mu-calculus is more expressive than LTL, CTL and CTL*.

Anyway, until there isn't any useful information on the mu-calculus, I can live with the article being a redirect to the mu operator. eboy 10:13, 24 October 2006 (UTC)

the mu operator in recursive functions may seem similar to the one in mu-calculus, but they are different.

the $\mu f=f(\mu f)$ in mu-calculus is a least fixed point operator, while the minimal or mu operator in partial recursive functions is the least natural satisfying some condition, is part of partial recursive functions, because the solution may not exist, i.e. one can iterate from zero, and keep testing every natural without finding an answer, i.e. the computation does not stop, so it is a partial function on the contrary of total functions that always stop, meaning that they are defined for every element in their domain.

As you can see both may use the Greek mu letter, they may both refer to words similar in natural English, (least - minimal), but they are part of different formal systems.

For that reason, NEVER MERGE mu-calculus and mu-operator articles, PLEASE. A disambiguation page of the mu symbol in formal systems may be added instead, if you wish. — Preceding unsigned comment added by 189.135.97.125 (talk) 18:37, 15 June 2011 (UTC)

I am new to mu-calculus, but I have a suggestion on notation that looks strange for me compairing with the usual notation in formal semantics

Should this text:

Given a labelled transition system $(S,R,V)$ and an interpretation $i:VAR\rightarrow 2^{S}$, we interpret a formula:

• $||p||_{i}=V(p)$;
• $||\phi \wedge \psi ||_{i}=||\phi ||_{i}\cap ||\psi ||_{i}$;
• $||\neg \phi ||_{i}=S\backslash ||\phi ||_{i}$;
• $||[a]\phi ||_{i}=\{s\in S\mid \forall t\in S,(s,t)\in R_{a}\rightarrow t\in ||\phi ||_{i}\}$;
• $||\nu Z.\phi ||_{i}=\bigcup \{T\subseteq S\mid T\subseteq ||\phi ||_{i[Z:=T]}\}$.

be rewritten as:

Given a labelled transition system $(S,R,V)$ and an interpretation :$[\![\ {\underline {\ }}\ ]\!]_{i}:{VAR}\rightarrow 2^{S}$, we interpret a formula:

• $[\![p]\!]_{i}=V(p)$;
• $[\![\phi \wedge \psi ]\!]_{i}=[\![\phi ]\!]_{i}\cap [\![\psi ]\!]_{i}$;
• $[\![\neg \phi ]\!_{i}=S\backslash [\![\phi ]\!]_{i}$;
• $[\![[a]\phi ]\!]_{i}=\{s\in S\mid \forall t\in S,(s,t)\in R_{a}\rightarrow t\in [\![\phi ]\!]_{i}\}$;
• $[\![\nu Z.\phi ]\!]_{i}=\bigcup \{T\subseteq S\mid T\subseteq [\![\phi ]\!]_{i[Z:=T]}\}$.

with $[\![\varphi ]\!]_{i}$ notation instead of the $||\varphi ||_{i}$ operator?

Your are right, other authors, (Winskel for example) use the notation that you suggest, I think it is more clear in this context, Stirling also is a well known researcher in this area, the cited article below [1], is very good, but I think that in this context the double bracket notation is more clear, any way it is defined in the article, and people working on this themes should be aware that there are many variations in notation always exist, and the subtle differences are only grasped when one goes deeper in the subject. Stirling uses $|\!|{\underline {~~}}|\!|_{\mathfrak {V}}^{\mathfrak {I}}$ in the article cited below, which I find potential problematic to render in many browsers, the $||{\underline {~~}}||_{i}$, besides of not being aesthetic, may cause some confusion to newbies thinking in more common uses of the $|\!|{\underline {~\,}}|\!|$ operator in other branches of mathematics, for that reason I changed the notation with double brackets, which is also correct.

Also I have the doubt, which of:

• $[\![\nu Z.\phi ]\!]_{i}=\bigcup \{T\subseteq S\mid T\subseteq [\![\phi ]\!]_{i[Z:=T]}\}$

or

• $[\![\nu Z.\phi ]\!]_{i}=\bigcup \{T\subseteq S\mid T\subseteq [\![\phi ]\!]_{i}[Z:=T]\}$

or even:

• $[\![\nu Z.\phi ]\!]_{i}=\bigcup \{T\subseteq S\mid T\subseteq [\![\phi [Z:=T]]\!]_{i}\}$

if any, is the correct one?

This rule looks wrong for me (in any of the versions), because z is a variable that may be replaced by a formula, the substitution [z:=T] replaces z, a formula, by T. if T is a set of states, that substitution seems wrong, because T does not belong to the set of formulas. Suppose that the substitution, which is a function $\{x\mapsto m_{1},y\mapsto m_{2},z\mapsto m_{3},\ldots \}$ is applied to an interpretation, what does it means something like $\{x\mapsto m_{1},y\mapsto m_{2},z\mapsto m_{3}\}[z:=\{1,2,3\}]$?

Are not fixed point operators involved in the rule for the $[\![\mu x.\varphi ]\!]_{i}$?

— Preceding unsigned comment added by 189.178.236.253 (talk) 21:44, 7 August 2012 (UTC)

First let me disclaim that I didn't write most of this article. As for your first point, I agree that notation you suggest is usually more common in CompSci (although the other one appears for this topic in [1]). For your last question, the semantics of $\mu$ can be derived from $\mu Z.\phi$ means $\neg \nu Z.\neg \phi (\neg Z)$,

I think what Tijfo means is: $\mu Z.\phi$ means $\neg \nu Z.\neg \phi [Z:=\neg Z]$ where $[X:=\neg X]$ is substitution, as usual.

where $\phi (\neg Z)$ and the other semantic rules. A derived formula would surely help the reader. I'll have to check some sources for your middle question/issue. It's been a while since I read anything about this topic. Tijfo098 (talk) 12:35, 26 October 2012 (UTC)

As for your first bit, there's an error in it because $i$ is just the interpretation of the variables, I've clarified that in the article. The notation $||p||_{i}=V(p)$ (for example) is meant to suggest that the interpretation of the formulas depends on the choice of the function i used to interpret variables (i is a pretty confusing notation for a function, I agree). Bradfield and Stirling write it with an "exponent" as well $||p||_{i}^{\mathfrak {S}}=V(p)$ to emphasize that it depends on the labeled transition system ${\mathfrak {S}}=(S,V,R)$ too; they also use ${\mathfrak {V}}$ instead of i, which is a less confusing notation. Tijfo098 (talk) 14:32, 26 October 2012 (UTC)

I've also clarified what $||\phi ||_{i[Z:=T]}$ means. It was "correct as formula", but a bit meaningless without an explanation because $i[Z:=T]$ is actually a somewhat conventional notation for a mapping identical to i everywhere but in Z, which it maps to T instead. Tijfo098 (talk) 15:08, 26 October 2012 (UTC)

I think that the confusion of the one who posted this section, is due to the misunderstanding of which formulas are the range of Z, and because I think that you have in mind the denotational semantics of Rec, the abstract functional language.

Think about Z as a subformula of $\phi$ which is the least that stay in a fixed point. This is similar of what you are thinking on, but more general, do not restrict yourself to think it as the factorial defined with a fixed point combinator like Y or $\Theta$ in lambda-calculus. The mu-calculus is (a dynamic logic) used to think about processes in general, which may behave like a total function, but that is the less interesting case. Processes are hard to grasp, I recommend the Formal Semantics book written by Glynn Winskel, for the concepts that you have, It will be clear for you. Although I think that the best book to read about any subject is the one that has a concrete description of the subject which one can understand with each one's background, not necessarily the most complete or newest.

A doubt in the historic origin of the $\mu z.\phi$ notation

I think that the historic origin of the notation should be confirmed before asserting this:

... are in the variable Z, much like in lambda calculus $\lambda Z.::\phi$ is a function with formula $\phi$ in bound variable Z; see the denotational semantics below for details.

I am not sure if this notation was inspired from lambda calculus as asserted in the article, because it is more close to the minimization operator in Recursive Functions. — Preceding unsigned comment added by 189.135.127.121 (talk) 20:12, 7 June 2013 (UTC)

External links modified (February 2018)

Hello fellow Wikipedians,

I have just modified one external link on Modal μ-calculus. Please take a moment to review my edit. If you have any questions, or need the bot to ignore the links, or the page altogether, please visit this simple FaQ for additional information. I made the following changes:

• Added archive https://web.archive.org/web/20160305061922/http://philo.ruc.edu.cn/logic/reading/Yde/mu0612.pdf to http://philo.ruc.edu.cn/logic/reading/Yde/mu0612.pdf

When you have finished reviewing my changes, you may follow the instructions on the template below to fix any issues with the URLs.

This message was posted before February 2018. After February 2018, "External links modified" talk page sections are no longer generated or monitored by InternetArchiveBot. No special action is required regarding these talk page notices, other than regular verification using the archive tool instructions below. Editors have permission to delete these "External links modified" talk page sections if they want to de-clutter talk pages, but see the RfC before doing mass systematic removals. This message is updated dynamically through the template {{source check}} (last update: 18 January 2022).

• If you have discovered URLs which were erroneously considered dead by the bot, you can report them with this tool.
• If you found an error with any archives or the URLs themselves, you can fix them with this tool.

Cheers.—InternetArchiveBot (Report bug) 07:16, 3 February 2018 (UTC)