LB4TL: A Smooth Semantics for Temporal Logic to Train Neural Feedback Controllers
Navid Hashemi, Samuel Williams, Bardh Hoxha, Danil V. Prokhorov, Georgios Fainekos, Jyotirmoy V. Deshmukh · IFAC-PapersOnLine · 2024
This paper presents a framework for training neural network (NN)-based feedback controllers for autonomous agents with deterministic nonlinear dynamics to satisfy task objectives and safety constraints expressed in discrete-time Signal Temporal Logic (DT-STL). Control synthesis that uses the robustness semantics of DT-STL poses challenges due to its non-convexity, non-differentiability, and recursive definition, in particular when it is used to train NN-based controllers. We introduce a smooth neuro-symbolic computation graph to encode DT-STL robustness to represent a smooth approximation of the robustness, enabling the use of powerful stochastic gradient descent and backpropagation-based optimization for training. Our approximation guarantees that it lower bounds the robustness value of a given DT-STL formula, and shows orders of magnitude improvement over existing smooth approximations when applied to control synthesis. We demonstrate our approach on planning to satisfy complex spatio-temporal and sequential tasks, and show scalability with formula complexity.