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

Onderzoeksoutput: Bijdrage aan tijdschriftTijdschriftartikelAcademicpeer review

16 Citaten (Scopus)
1 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 µ-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
Pagina's (van-tot)3129-3139
TijdschriftTheoretical Computer Science
Volume412
Nummer van het tijdschrift28
DOI's
StatusGepubliceerd - 2011

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

  • Citeer dit