Allen linear (interval) temporal logic - Translation to LTL and monitor synthesis

Grigore Roşu, Saddek Bensalem

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 ω-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.

Original languageEnglish (US)
Title of host publicationComputer Aided Verification - 18th International Conference, CAV 2006, Proceedings
PublisherSpringer
Pages263-277
Number of pages15
ISBN (Print)354037406X, 9783540374060
DOIs
StatePublished - 2006
Event18th International Conference on Computer Aided Verification, CAV 2006 - Seattle, WA, United States
Duration: Aug 17 2006Aug 20 2006

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4144 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other18th International Conference on Computer Aided Verification, CAV 2006
Country/TerritoryUnited States
CitySeattle, WA
Period8/17/068/20/06

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'Allen linear (interval) temporal logic - Translation to LTL and monitor synthesis'. Together they form a unique fingerprint.

Cite this