Resilient satisfaction of persistent and safety specifications by autonomous systems

Persistent and safety specifications appear in numerous applications including, but not limited to, search and rescue, aerial monitoring, pick-up and delivery. Such specifications may require visiting a region periodically, bounding a state in a desired interval, or keeping a distance with obstacles. One compact and rigorous way of defining these specifications is via Signal Temporal Logic (STL), which is a rich specification language for time-constrained behaviors. STL is endowed with a metric called robustness degree, which quantifies how well a trajectory satisfies a given STL formula. This metric enables the use of optimization methods to synthesize controllers for robust satisfaction of STL formulae. In this paper, we show that maximizing the robustness degree generally does not provide resilience, i.e., it does not facilitate recovery after a specification is violated. We propose a novel formulation for the synthesis of resilient controllers. Specifically, given an STL formula, we define a shifting STL formula, whose structure is the same as the original STL formula but its time windows capture the remaining mission horizon. We find the optimal control that maximizes the robustness degree with respect to the shifting STL formula. In some cases, the resulting control not only is a maximizer of the robustness degree with respect to the original formula but also provides resilience to the system. We illustrate the proposed method with a simulation case study.