Time window temporal logic
Files
Accepted manuscript
Date
2017-08-29
Authors
Vasile, Cristian-Ioan
Aksaray, Derya
Belta, Calin
Version
OA Version
Citation
Cristian-Ioan Vasile, Derya Aksaray, Calin Belta. 2017. "Time window temporal logic." THEORETICAL COMPUTER SCIENCE, v. 691, pp. 27 - 54 (28).
Abstract
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.
Description
License
© 2017 Elsevier B.V. All rights reserved.