A linear translation from LTL to the first-order modal µ-calculus

Research output: Book/ReportReportAcademic

39 Downloads (Pure)

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 languageEnglish
Place of PublicationEindhoven
PublisherTechnische Universiteit Eindhoven
Publication statusPublished - 2010

Publication series

NameComputer science reports
Volume1009
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.