Allen Linear (Interval) Temporal Logic --Translation to LTL and Monitor Synthesis--

Rosu, Grigore; Bensalem, Saddek

Permalink

https://hdl.handle.net/2142/11153 Copy

Description

Title

Allen Linear (Interval) Temporal Logic --Translation to LTL and Monitor Synthesis--

Author(s)

• Rosu, Grigore
• Bensalem, Saddek

Issue Date

2006-01

Keyword(s)

computer science

Abstract

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 \omega-sequences of timepoints, like in \LTL. It is shown that any \ALTL formula can be linearly translated into an equivalent \LTL formula, thus enabling the use of \LTL techniques and tools when requirements are expressed in \ALTL. %This translation also implies the NP-completeness of \ATL satisfiability. Then the monitoring problem for \ALTL is discussed, showing that it is NP-complete despite the fact that the similar problem for \LTL is EXPSPACE-complete. An effective monitoring algorithm for \ALTL is given, which has been implemented and experimented with in the context of planning applications.

Type of Resource

text

Permalink

http://hdl.handle.net/2142/11153

Copyright and License Information

You are granted permission for the non-commercial reproduction, distribution, display, and performance of this technical report in any format, BUT this permission is only for a period of 45 (forty-five) days from the most recent time that you verified that this technical report is still available from the University of Illinois at Urbana-Champaign Computer Science Department under terms that include this permission. All other rights are reserved by the author(s).

Owning Collections