ESE Ph.D. Thesis Defense – “Robustness of Temporal Logics with Applications to Safe Autonomy”

Signal Temporal Logic (STL) is a common way to express a broad range of real-time constraints that can be imposed on control systems. Spatial robustness of STL specifications, quantifying permissible spatial perturbations, has been widely studied in the literature. However, despite the importance of various time-critical systems, temporal robustness of STL has not yet been studied in depth nor has been used for control design.

In the first part of this thesis, we establish a comprehensive theoretical framework for temporal robustness of STL. 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 underlying signal temporal logic specification. We further prove that synchronous temporal robustness upper bounds asynchronous temporal robustness. Moreover, we show under which conditions these two robustness notions are equivalent. Introduced synchronous and asynchronous notions are directional and consider either left or right perturbations. Due to this reason we additionally define and study the combined temporal robustness which simultaneously considers left and right time shifts.

In the second part of this thesis, we focus on applications of various robustness functions to robust planning and control design questions. We first propose solutions to the temporally-robust control synthesis problem by presenting Mixed-Integer Linear Programming (MILP) encodings for derived temporal robustness notions. Second, we solve the spatially-robust control synthesis problem and show how to adapt the smooth operator for space robustness maximization. Furthermore, we propose possible distributed solutions to centralized multi-agent planning problems. Through various simulations, as well as experiments on actual robotic systems, we show that our presented solutions are computationally efficient as well as can be used in a wide variety of applications.