Temporal Robustness of Temporal Logic Specifications: Analysis and Control Design

TL;DR

This paper introduces the concept of temporal robustness in temporal logic specifications, analyzing its properties and proposing control design methods to maximize robustness in time-critical systems, with practical case studies.

Contribution

It defines synchronous and asynchronous temporal robustness, establishes their relationship, and develops a MILP-based control design approach to optimize robustness in dynamical systems.

Findings

Synchronous temporal robustness bounds asynchronous robustness.

Control design using synchronous robustness is more computationally efficient.

Case studies demonstrate the effectiveness of the proposed methods.

Abstract

We study the temporal robustness of temporal logic specifications and show how to design temporally robust control laws for time-critical control systems. This topic is of particular interest in connected systems and interleaving processes such as multi-robot and human-robot systems where uncertainty in the behavior of individual agents and humans can induce timing uncertainty. Despite the importance of time-critical systems, temporal robustness of temporal logic specifications has not been studied, especially from a control design point of view. We define synchronous and asynchronous temporal robustness and show that these notions quantify the robustness with respect to synchronous and asynchronous time shifts in the predicates of the temporal logic specification. It is further shown that the synchronous temporal robustness upper bounds the asynchronous temporal robustness. We then study the control design problem in which we aim to design a control law that maximizes the temporal robustness of a dynamical system. Our solution consists of a Mixed-Integer Linear Programming (MILP) encoding that can be used to obtain a sequence of optimal control inputs. While asynchronous temporal robustness is arguably more nuanced than synchronous temporal robustness, we show that control design using synchronous temporal robustness is computationally more efficient. This trade-off can be exploited by the designer depending on the particular application at hand. We conclude the paper with a variety of case studies.