### Abstract

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.

Original language | English |
---|---|

Place of Publication | Eindhoven |

Publisher | Technische Universiteit Eindhoven |

Publication status | Published - 2010 |

### Publication series

Name | Computer science reports |
---|---|

Volume | 1009 |

ISSN (Print) | 0926-4515 |

## Fingerprint Dive into the research topics of 'A linear translation from LTL to the first-order modal µ-calculus'. Together they form a unique fingerprint.

## Cite this

Cranen, S., Groote, J. F., & Reniers, M. A. (2010).

*A linear translation from LTL to the first-order modal µ-calculus*. (Computer science reports; Vol. 1009). Technische Universiteit Eindhoven.