<p>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 formulae in any of these logics (CTL,CTL* or LTL) to the μ-calculus?</p>

<p>Thanks very much in advance!</p>

CC BY-SA 3.0
2013-11-20T21:02:28.530Z
http://www.win.tue.nl/~jfg/articles/CSR-10-09.pdf It's doable.
Chad Brewbaker
CC BY-SA 3.0
2013-11-20T21:31:48.923Z
I am confused as to why you are asking this question, given that I answered your cs.stackexchange question with references. http://cs.stackexchange.com/a/16610/163
Vijay D
CC BY-SA 3.0
2013-11-20T22:01:47.720Z
First, thanks for your answer. I just thought that the question is hidden in the discussion and hoped that more people will see it as a stand alone question. Cheers
Dimiter
CC BY-SA 3.0
2013-11-22T18:33:14.723Z
In addition to Vijay D's comment, you also asked the exact same question [Techniques (tools) to convert temporal logic (CTL,CTL* or LTL) to μ-calculus formulae](http://cs.stackexchange.com/questions/18196/techniques-tools-to-convert-temporal-logic-ctl-ctl-or-ltl-to-calculus-for/18200#18200) 2 days ago and I also suggested an answer.
J.-E. Pin
<lo.logic><program-verification><temporal-logic>
Conversion technique/tool from temporal logic CTL,CTL* or LTL to μ-calculus
Dimiter
# Conversion technique/tool from temporal logic CTL,CTL* or LTL to μ-calculus

(Asked by: username_0 on 2013-11-20)

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 formulae in any of these logics (CTL,CTL\* or LTL) to the μ-calculus?

Thanks very much in advance!

**Tags:** lo.logic, program-verification, temporal-logic
> **Comments:**
> **username_1**: http://www.win.tue.nl/~jfg/articles/CSR-10-09.pdf It's doable.  
> **username_2**: I am confused as to why you are asking this question, given that I answered your cs.stackexchange question with references. http://cs.stackexchange.com/a/16610/163  
> **username_0**: First, thanks for your answer. I just thought that the question is hidden in the discussion and hoped that more people will see it as a stand alone question. Cheers  
> **username_3**: In addition to Vijay D's comment, you also asked the exact same question [Techniques (tools) to convert temporal logic (CTL,CTL* or LTL) to μ-calculus formulae](http://cs.stackexchange.com/questions/18196/techniques-tools-to-convert-temporal-logic-ctl-ctl-or-ltl-to-calculus-for/18200#18200) 2 days ago and I also suggested an answer.  

---

## 0 answers

