Time Window Temporal Logic

TL;DR

This paper presents time window temporal logic (TWTL), a language for specifying time-bounded tasks, along with automata-based methods for synthesis, verification, and learning, demonstrated through case studies.

Contribution

The paper introduces TWTL, a new expressive logic for time-bounded specifications, and develops automata-based algorithms for synthesis, verification, and relaxation of these specifications.

Findings

TWTL effectively describes serial tasks in robotics and control.

Automata-based algorithms enable efficient synthesis and verification.

Case studies demonstrate the logic's expressivity and algorithm effectiveness.

Abstract

This paper introduces time window temporal logic (TWTL), a rich expressivity language for describing various time bounded specifications. In particular, the syntax and semantics of TWTL enable the compact representation of serial tasks, which are typically seen in robotics and control applications. This paper also discusses the relaxation of TWTL formulae with respect to deadlines of tasks. Efficient automata-based frameworks to solve synthesis, verification and learning problems are also presented. 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 specification. Case studies illustrating the expressivity of the logic and the proposed algorithms are included.