Anzeige
Erschienen in:
2006 | OriginalPaper | Buchkapitel
Allen Linear (Interval) Temporal Logic – Translation to LTL and Monitor Synthesis
verfasst von : Grigore Roşu, Saddek Bensalem
Erschienen in: Computer Aided Verification
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
The relationship between two well established formalisms for temporal reasoning is first investigated, namely between Allen’s interval algebra (or Allen’s temporal logic, abbreviated
ATL
) and linear temporal logic (
LTL
). A discrete variant of
ATL
is defined, called Allen linear temporal logic (
ALTL
), whose models are
ω
-sequences of timepoints. It is shown that any
ALTL
formula can be linearly translated into an equivalent
LTL
formula, thus enabling the use of
LTL
techniques on
ALTL
requirements. This translation also implies the NP-completeness of
ATL
satisfiability. Then the problem of monitoring
ALTL
requirements is investigated, showing that it reduces to checking satisfiability; the similar problem for unrestricted
LTL
is known to require exponential space. An effective monitoring algorithm for
ALTL
is given, which has been implemented and experimented with in the context of planning applications.