Control Synthesis using Signal Temporal Logic Specifications with Integral and Derivative Predicates

TL;DR

This paper enhances Signal Temporal Logic (STL) with integral and derivative predicates, enabling more expressive control specifications that incorporate signal dynamics, and demonstrates their effectiveness through mixed-integer linear programming for autonomous robot control.

Contribution

Introduces new integral and derivative predicates into STL, encoded as MILP constraints, to improve control synthesis with richer signal property specifications.

Findings

New predicates improve control trajectory quality.

Enhanced STL expressiveness for complex signal properties.

Case study shows practical benefits in robot control.

Abstract

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.