TY - BOOK
T1 - A linear translation from LTL to the first-order modal µ-calculus
AU - Cranen, S.
AU - Groote, J.F.
AU - Reniers, M.A.
PY - 2010
Y1 - 2010
N2 - The modal µ-calculus is a very expressive temporal logic. In particular, logics such as LTL, CTL and CTL* can be translated into the modal mu-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.
AB - The modal µ-calculus is a very expressive temporal logic. In particular, logics such as LTL, CTL and CTL* can be translated into the modal mu-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.
M3 - Report
T3 - Computer science reports
BT - A linear translation from LTL to the first-order modal µ-calculus
PB - Technische Universiteit Eindhoven
CY - Eindhoven
ER -