Control Synthesis using Signal Temporal Logic Specifications with Integral and Derivative Predicates
This work addresses the need for richer temporal logic specifications in control systems, particularly for applications where cumulative or rate-based signal information is critical, representing an incremental advancement in formal methods for robotics and autonomous systems.
The paper tackles the problem of expressing complex signal properties like integrals and derivatives in control synthesis by extending Signal Temporal Logic (STL) with new predicates, resulting in a method that encodes these into mixed-integer linear inequalities to find trajectories satisfying specifications, as demonstrated in an autonomous robot case study.
In many applications, the integrals and derivatives of signals carry valuable information (e.g., cumulative success over a time window, the rate of change) regarding the behavior of the underlying system. In this paper, we extend the expressiveness of Signal Temporal Logic (STL) by introducing predicates that can define rich properties related to the integral and derivative of a signal. For control synthesis, the new predicates are encoded into mixed-integer linear inequalities and are used in the formulation of a mixed-integer linear program to find a trajectory that satisfies an STL specification. We discuss the benefits of using the new predicates and illustrate them in a case study showing the influence of the new predicates on the trajectories of an autonomous robot.