Reachability-based Control Synthesis under Signal Temporal Logic Specifications

TL;DR

This paper presents a reachability-based control synthesis method for linear disturbed systems under Signal Temporal Logic specifications, using zonotope techniques to decompose and solve local control problems ensuring global compliance.

Contribution

It introduces a novel approach combining zonotope-based state space partitioning, STL formula decomposition, and reachability analysis for control synthesis under complex temporal and spatial constraints.

Findings

Successfully synthesizes controllers satisfying STL specifications.

Demonstrates effectiveness through a numerical example.

Integrates zonotope techniques with reachability analysis for control design.

Abstract

In this paper, we investigate the controller design problem for linear disturbed systems under signal temporal logic (STL) specifications imposing both spatial and temporal constraints on system behavior. We first implement zonotope-based techniques to partition the state space into finite cells, then propose an evaluation mechanism to rearrange the time constraints of the STL specification, and finally decompose the global STL formula into finite local STL formulas. In this way, each cell has a local control design problem, which is further formulated into a local optimization problem. To deal with each local optimization problem, we take advantage of the properties of zonotopes and reachability analysis to design local controller consisting of feedforward and feedback parts. By solving all local optimization problems, all local controllers are combined to guarantee the global STL specification. Finally, a numerical example is presented to illustrate the derived results.