All Questions
Tagged with linear-temporal-logic mu-calculus
2 questions
1
vote
1
answer
820
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