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 -