2
$\begingroup$

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!

Improve this question
$\endgroup$
4

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.