Anzeige
Erschienen in:
2007 | OriginalPaper | Buchkapitel
Regular Linear Temporal Logic
verfasst von : Martin Leucker, César Sánchez
Erschienen in: Theoretical Aspects of Computing – ICTAC 2007
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
We present regular linear temporal logic (RLTL), a logic that generalizes linear temporal logic with the ability to use regular expressions arbitrarily as sub-expressions. Every LTL operator can be defined as a context in regular linear temporal logic. This implies that there is a (linear) translation from LTL to RLTL.
Unlike LTL, regular linear temporal logic can define all
ω
-regular languages, while still keeping the satisfiability problem in PSPACE. Unlike the extended temporal logics
$\text{ETL}_*$
, RLTL is defined with an algebraic signature. In contrast to the linear time
μ
-calculus, RLTL does not depend on fix-points in its syntax.