Signal Temporal Logic Meets Reachability: Connections and Applications

Abstract

Signal temporal logic (STL) and reachability analysis are effective mathematical tools for formally analyzing the behavior of robotic systems. STL is a specification language that uses logic and temporal operators to precisely express real-valued and time-dependent requirements on system behaviors. While recursively defined STL specifications are extremely expressive and controller synthesis methods exist, there has not been work that quantifies the set of states from which STL formulas can be satisfied. Reachability analysis, on the other hand, involves computing the reachable set – the set of states from which a system is able to reach a goal while satisfying state and control constraints. While reasoning about system requirements through sets of states is useful for predetermining the possibility of satisfying desired system properties and obtaining state feedback controllers, so far the application of reachability has been limited to reach-avoid specifications. In this paper, we merge STL and time-varying reachability into a single framework that combines the key advantage of both methods – expressiveness of specifications and set quantification. To do this, we establish a correspondence between temporal and reachability operators, and use the idea of least-restrictive feasible controller sets (LRFCSs) to break down controller synthesis for complex STL formulas into a sequence of reachability and elementary set operations. LRFCSs are crucial for avoiding controller conflicts among different reachability operations. In addition, the synthesized state feedback controllers are guaranteed to satisfy STL specifications if determined to be possible by our framework, and violate specifications minimally if not. For simplicity, Hamilton-Jacobi reachability will be used in this paper, although our method is agnostic to the time-varying reachability method. We demonstrate our method through numerical simulations and robotic experiments.