The modal μ-calculus is a very expressive temporal logic. In particular, logics such as LTL, CTL and CTL~* can be translated into the modal μ-calculus, although existing translations of LTL and CTL~* are at least exponential in size. We show that an existing simple first-order extension of the modal μ-calculus allows for a linear translation from LTL Furthermore, we show that solving the translated formulae is as efficient as the best known methods to solve LTL formulae directly.
展开▼
