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

Onderzoeksoutput: Boek/rapportRapportAcademic

39 Downloads (Pure)

Samenvatting

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.
Originele taal-2Engels
Plaats van productieEindhoven
UitgeverijTechnische Universiteit Eindhoven
StatusGepubliceerd - 2010

Publicatie series

NaamComputer science reports
Volume1009
ISSN van geprinte versie0926-4515

Vingerafdruk Duik in de onderzoeksthema's van 'A linear translation from LTL to the first-order modal µ-calculus'. Samen vormen ze een unieke vingerafdruk.

  • Citeer dit

    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.