PaperlayerView exact revision on arXiv

Source-linked AI summary

Robust Temporal Logic Model Predictive Control

Sadra Sadraddini, Calin Belta

arXiv:1511.00347v1eess.SY

TL;DR

The paper addresses robust STL-constrained control for uncertain discrete-time linear systems. It develops a conservative mixed-integer MPC synthesis framework that maintains specifications when feasible and minimizes violations otherwise. The resulting receding-horizon controller is globally robust and cost-aware within the stated formulation.

  • Problem

    Existing MPC work largely targets simple objectives and constraints, motivating robust synthesis for richer STL specifications under disturbances.

  • Method

    The paper uses conservative uncertainty propagation and mixed-integer MPC, with softened STL predicates and penalized slack variables to recover feasibility.

  • Results

    The closed-loop controller globally satisfies the STL specification for all disturbance realizations when feasible and otherwise finds minimally violating controls.

  • Takeaways & Limitations

    The framework connects robust correctness, cost optimization, and minimal constraint violation within a computationally tractable receding-horizon controller.

Abstract

from arXiv · show

Control synthesis from temporal logic specifications has gained popularity in recent years. In this paper, we use a model predictive approach to control discrete time linear systems with additive bounded disturbances subject to constraints given as formulas of signal temporal logic (STL). We introduce a (conservative) computationally efficient framework to synthesize control strategies based on mixed integer programs. The designed controllers satisfy the temporal logic requirements, are robust to all possible realizations of the disturbances, and optimal with respect to a cost function. In case the temporal logic constraint is infeasible, the controller satisfies a relaxed, minimally violating constraint. An illustrative case study is included.

I. INTRODUCTION

The paper extends constrained MPC toward STL specifications for uncertain linear systems, seeking computationally tractable, robust control synthesis with minimally violating fallbacks.

  • MPC generates constrained, potentially suboptimal control strategies, but traditional objectives and constraints often focus on reference tracking.
  • Temporal logics express richer behavioral specifications, including recurring constraint satisfaction with deadlines.
  • Finite-abstraction temporal-logic control is correct by construction but generally expensive because it requires computing a finite-state representation.
  • The proposed MPC framework targets global STL satisfaction for discrete-time linear systems with additive bounded uncertainties using conservative, tractable uncertainty propagation.
  • When constraints are infeasible, the framework softens them to seek minimally violating solutions under uncertainties and limited actuation.
  • A related counterexample-guided approach may fail to terminate, become computationally intractable with many counterexamples, or encounter infeasibility without a global guarantee.

II. PROBLEM STATEMENT

The problem is to synthesize a receding-horizon controller for discrete-time systems that is robust and correct globally, optimizes cost, and minimizes violations when feasibility fails.

  • The system uses state x, admissible control u, bounded disturbances w, known plant matrices, and a stage cost J(x[t],u[t]).
  • STL combines logical connectives and bounded-time temporal operators over numerical predicates to specify system behavior.
  • Discrete-time synthesis does not generally guarantee validity of the corresponding STL formula for the original continuous-time system.
  • Predicates are represented as nonnegative linear output conditions, such as y_i[t] ≥ 0, with matrices determined by the specification.
  • STL robustness is a quantitative satisfaction measure: positive values indicate satisfaction, negative values indicate violation, and zero is treated as satisfaction by the algorithms.
  • The synthesis objective requires global robust correctness for every disturbance realization, receding-horizon cost optimality, and minimal violation when satisfaction is infeasible.

III. STL RECEDING HORIZON CONTROL

The controller uses STL horizons to predict the future robustness needed for receding-horizon decisions, updating controls online while maintaining past and future satisfaction.

  • The formula horizon h_ϕ determines which future secondary signals are needed to compute robustness.
  • Formula horizon and control-sequence horizon are distinct: the former concerns robustness dependence, while the latter defines searched controls.
  • At each time step, predicted secondary signals are used to enforce nonnegative robustness constraints spanning the relevant past and future times.
  • Only the current control is applied, and a new control sequence is computed after the next measurement.
  • If the receding-horizon problem remains feasible at every time, induction establishes global satisfaction of the STL specification in closed loop.
  • Longer prediction horizons may improve feasibility in principle but can become conservative or infeasible under uncertainty because they extend worst-case predictions.
  • Unlike the closest related scheme, this approach updates controls using both stored history and current measurements, supporting online adaptation under uncertainty.

IV. ROBUST STL SATISFACTION

The approach constructs robust MPC for STL control under bounded disturbances, using positive normal form to characterize uncertainty propagation into STL constraints.

  • The robust MPC mechanism seeks controls that satisfy STL constraints for all possible realizations of bounded disturbances.The approach first introduces positive normal form STL to characterize how uncertainty affects secondary signals and constraints.
  • Element-wise vector inequalities are used throughout the robust prediction and constraint formulations.

A. Positive Normal Form STL

Positive normal form makes STL robustness non-decreasing in secondary signals, enabling uncertainty propagation analysis and constraint softening while remaining computationally tractable.

  • A. Positive Normal Form STL: Positive normal form requires STL robustness to be non-decreasing with respect to secondary signals over the relevant horizon.This monotonicity enables bounds on uncertainty propagation into STL constraints and supports slack-based softening.
  • A. Positive Normal Form STL: STL formulas without negation are in positive normal form because their robustness uses only min and max operations without sign changes.
  • A. Positive Normal Form STL: Every STL formula can be transformed into positive normal form by recursively propagating negations and modifying secondary-signal signs.
  • A. Positive Normal Form STL: Predicate negations are removed by redefining a secondary signal or introducing a new signal with reversed sign.If both a predicate and its negation occur, the transformation introduces a separate secondary signal for the negated predicate.
  • A. Positive Normal Form STL: 30 The number of secondary signals can double in the worst case, while synthesis complexity is exponential in that number.

B. Robust Prediction System

The robust prediction system maps controls and bounded disturbances into finite-horizon secondary signals, then enforces STL constraints at a conservative lower-bound point of the uncertainty set.

  • B. Robust Prediction System: The finite-horizon secondary-signal prediction combines the current state, control sequence, disturbance propagation, and affine output terms.The system uses flow matrices to map state, controls, and disturbances into predicted secondary signals.
  • B. Robust Prediction System: Because robustness is generally non-convex, checking uncertainty-set vertices alone may fail to detect negative robustness inside the set.A parallelogram example has all vertices in the positive region while an interior section has negative robustness.
  • B. Robust Prediction System: The method enforces constraints at the lower-left corner of the axis-aligned minimum bounding box of the uncertainty image set.For positive-normal-form STL, this corner provides a robustness lower bound because the image-set secondary signals are element-wise larger.
  • B. Robust Prediction System: The lower-left bounding-box corner can be computed from the polytope representation and its vertices before control synthesis begins.
  • B. Robust Prediction System: Satisfying the robust prediction constraints guarantees satisfaction of the original open-loop constraints for positive-normal-form STL.
  • B. Robust Prediction System: The methodology extends to known time-varying system matrices, but unstable plant dynamics can make predictions conservative or infeasible over longer horizons.

V. OPTIMIZATION BASED CONTROL

The paper formulates optimality and minimal violation within an optimization problem and expresses that problem as a mixed integer program solvable by standard solvers.

  • V. OPTIMIZATION BASED CONTROL: The optimization formulation addresses both cost optimality and minimal STL-constraint violations.

A. Optimization Problem

The paper selects nominal-cost-optimal controls from those robustly satisfying STL constraints, while introducing slack minimization to recover feasibility when disturbances or actuation limits make satisfaction impossible.

  • The controller chooses the least finite-horizon nominal evolution cost among control sequences that robustly satisfy STL constraints.
  • Softened secondary signals and a nonnegative slack variable ζ enable minimally violating solutions when STL constraints are inevitably infeasible.Both robust prediction and history values are softened.
  • A large penalty M prioritizes ζ minimization under infeasibility and cost optimization when the STL constraints are feasible.Feasible problems enforce ζ = 0; infeasible problems minimize ζ without optimizing cumulative cost.
  • The smallest feasible softening value is characterized explicitly as ζmin.
  • The detailed proof relies on monotonicity of the robustness function for positive normal form STL formulas.
  • Different softening weights or multiple softening values may require tuning to identify a practically efficient strategy.

B. Mixed Integer Formulation

STL constraints are encoded as mixed-integer constraints by representing quantitative-semantics max/min operations recursively, with binary encoding chosen for greater computational efficiency.

  • Binary encoding represents STL quantitative semantics recursively and is computationally more efficient than directly encoding potentially large max/min argument sets.
  • For each predicate, a binary variable indicates whether the predicate is true or false at a given time.
  • Binary encoding the secondary signals requires p×(H+hϕ+1) binary variables, followed by recursively defined variables for the STL formula.
  • Conjunctions and disjunctions are encoded through recursively defined mixed-integer variables.
  • The resulting optimization problem is a MILP, MIQP, or MINLP depending on whether the cost function is linear, quadratic, or nonlinear.Because mixed-integer programs are exponentially expensive in the number of integer variables, real-time applications are restricted to small systems.

VI. CASE STUDY

The case study evaluates STL MPC on a disturbed double integrator requiring bounded oscillation, comparing nominal and robust control across disturbance and actuation settings.

  • The case study uses a two-dimensional double integrator with energy loss, scalar control input, bounded disturbances, and stage cost J(u[t]) = |u[t]|.The disturbance satisfies ∥w[t]∥∞≤w0, and the cost penalizes control effort.
  • The STL specification requires x1 to visit both [2,4] and [−4,−2] at least once within every five consecutive time steps.
  • With w0 = 0, the optimal-correct solution oscillates between x1 = 2 and x1 = 4 without entering the regions unnecessarily.Its robustness function remains zero.
  • At w0 = 0.2, nominal MPC fails the specification, with occasionally negative robustness values.
  • Robust MPC conservatively enters the specified regions and maintains robustness values above zero for w0 = 0.2.
  • For ∥w[t]∥∞≤0.5, the robust controller becomes infeasible over the long horizon, while reducing H to 5 or 4 yields better solutions.
  • With |u| ≤2 and disturbance bound 0.2, the controller cannot satisfy STL constraints but maximally oscillates to minimize violation.

VII. CONCLUSION AND FUTURE WORK

The paper develops STL MPC for discrete-time linear systems with bounded additive disturbances, linking optimality and correctness while identifying extensions to broader and distributed systems.

  • The paper connects optimality and correctness for discrete-time linear systems with additive bounded disturbances using STL-based model predictive control.
  • Future work targets piecewise affine systems, traffic networks, and distributed MPC using assume-guarantee reasoning for component disturbances.
Loading 1511.00347v1…