Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Direct data-driven control with signal temporal logic specifications

Birgit C. van Huijgevoort, Chris Verhoek, Roland Tóth, Sofie Haesaert

TL;DR

This work addresses the challenge of achieving formal STL guarantees without explicit system modeling by proposing a direct data‑driven control synthesis method for LTI systems. It leverages the Fundamental Lemma to obtain a data‑driven representation from a single input–output sequence and reformulates STL satisfaction as a MILP, enabling automatic controller synthesis that minimizes a quadratic IO cost. The approach extends to unbounded STL specifications through looping constructions and is demonstrated on car platoon and HVAC case studies, showing feasible computation times and practical viability. By eliminating the need for a full system model, the method reduces modeling errors and provides sound, provably correct control under STL constraints, with clear avenues for extension to nonlinear or noisy settings.

Abstract

Most control synthesis methods under temporal logic properties require a model of the system, however, identifying such a model can be a challenging task. In this work, we develop a direct data-driven control synthesis method for temporal logic specifications, which does not require this explicit modeling step, capable of providing certificates for the general class of linear systems. After collecting a single sequence of input-output data from the system, we construct a data-driven characterization of the behavior. Using this characterization, we synthesize a controller, such that the controlled system satisfies a (possibly unbounded) temporal logic specification. The underlying optimization problem is solved by mixed-integer linear programming. We demonstrate the applicability of the results through simulation examples.

Direct data-driven control with signal temporal logic specifications

TL;DR

This work addresses the challenge of achieving formal STL guarantees without explicit system modeling by proposing a direct data‑driven control synthesis method for LTI systems. It leverages the Fundamental Lemma to obtain a data‑driven representation from a single input–output sequence and reformulates STL satisfaction as a MILP, enabling automatic controller synthesis that minimizes a quadratic IO cost. The approach extends to unbounded STL specifications through looping constructions and is demonstrated on car platoon and HVAC case studies, showing feasible computation times and practical viability. By eliminating the need for a full system model, the method reduces modeling errors and provides sound, provably correct control under STL constraints, with clear avenues for extension to nonlinear or noisy settings.

Abstract

Most control synthesis methods under temporal logic properties require a model of the system, however, identifying such a model can be a challenging task. In this work, we develop a direct data-driven control synthesis method for temporal logic specifications, which does not require this explicit modeling step, capable of providing certificates for the general class of linear systems. After collecting a single sequence of input-output data from the system, we construct a data-driven characterization of the behavior. Using this characterization, we synthesize a controller, such that the controlled system satisfies a (possibly unbounded) temporal logic specification. The underlying optimization problem is solved by mixed-integer linear programming. We demonstrate the applicability of the results through simulation examples.
Paper Structure (18 sections, 2 theorems, 20 equations, 3 figures, 2 algorithms)

This paper contains 18 sections, 2 theorems, 20 equations, 3 figures, 2 algorithms.

Table of Contents

  1. Introduction
  2. Problem statement
  3. Notation
  4. Discrete-time dynamical systems
  5. Signal temporal logic specifications and cost function
  6. Problem statement
  7. Data-driven characterization of the system
  8. Direct data-driven temporal logic control synthesis
  9. Direct data-driven control for bounded specifications
  10. Soundness and completeness analysis
  11. Soundness.
  12. Completeness.
  13. Direct data-driven control for unbounded specifications
  14. Case studies
  15. Car platoon
  16. ...and 3 more sections

Key Result

Proposition 1

Let $T_{\text{ini}}+1 \geq \mathbf{l}(\mathfrak{B})$. Then for any given $\mathbf{w}^\text{ini} \in\left.\mathfrak{B} \right|_{[0,T_\text{ini}]}$ and $\mathbf{u}_{[0,L]} \in\left(\mathbb{R}^{n_\mathrm{u}}\right)^{L+1}$, there is a unique $\mathbf{y}_{[0,L]} \in\left(\mathbb{R}^{n_\mathrm{y}}\right)^

Figures (3)

  • Figure 1: Loop constraint (left) on the state and (right) on the signal $w$ composed of the input and output $(u,y)$.
  • Figure 2: Results of the car platoon problem for cost function ${J_1(\mathbf{u}_0,\mathbf{y}_0)=\|\mathbf{y}_{[0,L]}\|}$ and ${J_2(\mathbf{u}_0,\mathbf{y}_0)=\|\mathbf{u}_{[0,L]}\|}$, displayed in panels (a), (b) and (c), (d).
  • Figure 3: Room temperature (blue) at a specific time. The comfort level combined with the occupancy is given in red.

Theorems & Definitions (6)

  • Definition 1: Dynamical system
  • Proposition 1: Initial Condition
  • Definition 2
  • Proposition 2: Fundamental Lemma for control
  • Definition 3
  • Remark 1