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

Research output: Contribution to journalArticleAcademicpeer-review

18 Citations (Scopus)
1 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 µ-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
Pages (from-to)3129-3139
JournalTheoretical Computer Science
Volume412
Issue number28
DOIs
Publication statusPublished - 2011

Fingerprint

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

Cite this