Time window temporal logic

Cristian Ioan Vasile, Derya Aksaray, Calin Belta

Research output: Contribution to journalArticlepeer-review

36 Scopus citations


This paper introduces time window temporal logic (TWTL), a rich expressive language for describing various time bounded specifications. In particular, the syntax and semantics of TWTL enable the compact representation of serial tasks, which are prevalent in various applications including robotics, sensor systems, and manufacturing systems. This paper also discusses the relaxation of TWTL formulae with respect to the deadlines of the tasks. Efficient automata-based frameworks are presented to solve synthesis, verification and learning problems. The key ingredient to the presented solution is an algorithm to translate a TWTL formula to an annotated finite state automaton that encodes all possible temporal relaxations of the given formula. Some case studies are presented to illustrate the expressivity of the logic and the proposed algorithms.

Original languageEnglish (US)
Pages (from-to)27-54
Number of pages28
JournalTheoretical Computer Science
StatePublished - Aug 29 2017
Externally publishedYes

Bibliographical note

Funding Information:
This work was supported in part by NSF grants numbers NRI-1426907, NSF CMMI-1400167, and ONR grant number N00014-14-1-0554.

Publisher Copyright:
© 2017 Elsevier B.V.


  • Controller synthesis
  • Finite state automata
  • Temporal relaxation
  • Timed temporal logic
  • Unambiguous languages
  • Verification


Dive into the research topics of 'Time window temporal logic'. Together they form a unique fingerprint.

Cite this