PaperlayerView exact revision on arXiv

Source-linked AI summary

Model Predictive Control for Signal Temporal Logic Specification

Vasumathi Raman, Alexandre Donzé, Mehdi Maasoumy, Richard M. Murray, Alberto Sangiovanni-Vincentelli, Sanjit A. Seshia

arXiv:1703.09563v1eess.SYcs.FLcs.LOcs.SY

TL;DR

Cyber-physical systems with timed specifications pose challenges for automated correctness reasoning, while exhaustive verification or synthesis is generally undecidable. This paper encodes STL specifications as MILP constraints for open-loop and receding-horizon control, and reports controller-synthesis case studies with simulations illustrating the methodology’s effectiveness.

  • Problem

    Correctness reasoning for increasingly complex cyber-physical control interactions is challenging, and exhaustive synthesis for systems with timed behavior is generally undecidable.

    Source: §I · p. 1

  • Method

    The paper encodes STL specifications as MILP constraints for controller synthesis, including open-loop and receding-horizon formulations.

    Source: §I · pp. 1–2

  • Results

    Simulation results for HVAC and smart-micro-grid controller synthesis illustrate the effectiveness of framing the MPC schemes as synthesis from STL specifications.

    Source: §X · p. 11

  • Takeaways & Limitations

    The authors demonstrate control synthesis for systems on both the demand and supply sides of a smart grid using STL specifications.

    Source: §X · p. 11

Abstract

from arXiv · show

We present a mathematical programming-based method for model predictive control of cyber-physical systems subject to signal temporal logic (STL) specifications. We describe the use of STL to specify a wide range of properties of these systems, including safety, response and bounded liveness. For synthesis, we encode STL specifications as mixed integer-linear constraints on the system variables in the optimization problem at each step of a receding horizon control framework. We prove correctness of our algorithms, and present experimental results for controller synthesis for building energy and climate control.

I. INTRODUCTION

The paper addresses the difficulty of ensuring correctness across increasingly complex cyber-physical control layers and the limits of exhaustive verification or synthesis for systems with timed behavior. It proposes automatically encoding STL specifications for receding-horizon control, building on discrete-time system models and STL’s real-time temporal operators.

I. INTRODUCTION

  • Exhaustive verification or synthesis is generally undecidable for systems whose specifications depend on temporal distances, leaving simulation and testing as the method of choice.The introduction also identifies increasingly difficult correctness reasoning across interacting controller layers as a motivation for automation.Source: §I · p. 1
  • Two automatically generated MILP encodings represent STL specifications for cyber-physical-system control, supporting open-loop synthesis and use in an MPC framework.The encodings can target satisfaction or maximize quantitative robustness; the paper also gives an STL fragment whose synthesis becomes an LP under stated assumptions.Source: §I · p. 2

A. Systems

  • The system model represents continuous and logical states, control inputs, and disturbances with a discrete-time difference equation and a cost over runs.The model assumes a unique horizon-N run for a given initial state, input sequence, and disturbance sequence.Source: A. Systems · p. 2

B. Signal Temporal Logic

  • STL specifies real-valued signals with predicates and temporal operators, including bounded always and until operators over time intervals.A formula’s bound provides a conservative maximum trajectory length needed to decide satisfiability.Source: B. Signal Temporal Logic · p. 2
  • The paper focuses on discrete-time control; the relationship between continuous- and discrete-time STL semantics under discretization error and sampling time is outside its scope.The specification is intended to be independent of the sampling time.Source: B. Signal Temporal Logic · pp. 2–3

C. Quantitative semantics for STL

The paper defines quantitative STL semantics that assign a real-valued robustness score to a signal and time, then frames control synthesis as open-loop or receding-horizon optimization. Its formulation can encode satisfaction constraints and, without a separate run objective, maximize robustness.

C. Quantitative semantics for STL

  • STL robustness is computed recursively: predicate values seed the score, Boolean operators use min or max, and temporal operators aggregate scores across time.A positive score implies satisfaction; the score’s absolute value is described as a signed distance in projections defined by the predicates.Source: C. Quantitative semantics for STL · p. 3

III. PROBLEM STATEMENT

  • The synthesis problems take an STL formula, cost, initial state, horizon, and reference disturbance as inputs, with the state assumed fully observable and disturbances known in advance.The paper considers both open-loop and closed-loop synthesis.Source: §III · p. 3
  • The closed-loop problem uses a horizon L shorter than N and computes the first control input at each step, corresponding to an MPC scheme.The reference disturbance may change at each iteration.Source: §III · p. 3
  • STL constraints combine with system-dynamics constraints in a MILP optimization, and robustness is maximized when no run objective is supplied.The paper presents open-loop and closed-loop solutions for a large class of STL formulas.Source: §III · p. 3

IV. OPEN-LOOP CONTROLLER SYNTHESIS

Open-loop synthesis searches for a finite control trajectory satisfying an STL specification, using system, loop, and STL constraints in an MILP. For infinite-horizon specifications, a finite lasso-shaped trajectory represents an infinite run, with a conservative search for infinite-state systems.

IV. OPEN-LOOP CONTROLLER SYNTHESIS

  • Open-loop synthesis extends bounded model checking to dynamical systems using mixed-integer programming and searches for a trajectory satisfying the STL formula.For infinite runs, the approach uses a finite sequence with a loop; this is conservative for infinite-state systems, while for finite-state systems the lasso structure is without loss of generality.Source: §IV · p. 3
  • The open-loop problem uses the STL formula, discrete-time plant model, cost, initial state, and disturbance to generate control inputs over N steps.The resulting MILP includes system, loop, and STL constraints.Source: Figure 1 · p. 3, §IV · p. 3

A. Constraints on system evolution

  • System constraints encode valid horizon-N trajectories and apply when the system dynamics, constraints, and objectives admit an MILP formulation.The paper gives smart-grid regulation and mixed logical dynamical systems as examples.Source: A. Constraints on system evolution · p. 4

B. Loop constraints for trajectory parametrization

  • Loop constraints let a finite path represent an infinite one by requiring its final state to equal an earlier state.Binary variables select the loop point; when a variable is active, the corresponding earlier state equals the final state.Source: B. Loop constraints for trajectory… · p. 4

1) Predicates:

  • The predicate encoding uses binary variables to represent whether each linear predicate holds at each time step.The encoding requires sufficiently large positive M_t and sufficiently small positive ε_t values to bound predicate values away from zero.Source: 1) Predicates · p. 4

2) Boolean operations on MILP variables:

The Boolean and temporal encodings build STL constraints recursively from variables representing formula truth. These constraints can be combined with system and loop constraints to check feasibility or optimize a trajectory satisfying the specification.

2) Boolean operations on MILP variables:

  • Binary variables represent whether predicates and their formula operands hold at each time step, providing the building blocks for recursive Boolean-operation encodings.The paper says these Boolean-variable definitions are consistent with.Source: 2) Boolean operations on MILP variables · p. 4

3) Temporal constraints:

  • The bounded always encoding requires a formula to hold at every time in its interval, while the bounded eventually encoding requires it to hold at some time in that interval.Both intervals are relative to the current time step.Source: 3) Temporal constraints: □ · p. 4
  • The bounded until operator is defined using unbounded until, whose infinite-trajectory encoding uses an auxiliary constraint to prevent circular reasoning on finite representations.The auxiliary encoding is attributed to.Source: 3) Temporal constraints: □ · pp. 4–5
  • Combining STL, loop, and system constraints yields an MILP that can be checked for feasibility or optimized for a cost over system runs.The paper’s algorithm assembles these constraint sets to solve the open-loop problem.Source: 3) Temporal constraints: □ · p. 5

D. Quantitative Encoding

The quantitative encoding represents STL satisfaction robustness with recursively generated MILP constraints. Robustness can serve as an optimization objective and can make specification constraints easier to relax, but introduces computational costs.

D. Quantitative Encoding

  • The encoding recursively introduces robustness variables and MILP constraints, with positive robustness corresponding to formula satisfaction.The robustness value is computed along the formula structure.Source: D. Quantitative Encoding · p. 5
  • Maximizing the initial robustness value yields a trajectory with maximized satisfaction robustness, and robustness constraints can be softened or hardened.A limited violation can be allowed by requiring robustness greater than −ϵ.Source: D. Quantitative Encoding · pp. 5–6
  • The robustness encoding uses additional binary variables for formula operators, making it more expensive to compute in practice.Max and min operations are expressed in MILP using additional binary variables.Source: D. Quantitative Encoding · pp. 5–6
  • Including robustness as an objective makes the cost function non-convex, potentially with many local minima, though relaxed robustness constraints can permit a simpler cost function.The simpler cost function can make the problem more tractable.Source: D. Quantitative Encoding · p. 6

E. Complexity

The section characterizes MILP size and identifies an STL fragment for which the encoding preserves convexity and admits polynomial-time synthesis. General synthesis remains computationally challenging as problem dimensions grow.

E. Complexity

  • General synthesis has MILP complexity and is NP-hard, making it computationally challenging as problem dimensions grow.The number of binary variables for predicate satisfaction depends directly on the predicates in the STL formula.Source: E. Complexity · p. 6
  • Boolean encoding uses O(N·|P|) binary and O(N·|ϕ|) continuous variables; robustness encoding uses O(N·|P|) continuous and O(N·|ϕ|) binary variables.Here |P| counts predicates and |ϕ| counts formula operators.Source: E. Complexity · p. 6
  • SNN-STL restricts negations to atomic propositions, allows only □ temporal operators, and permits conjunctions but not disjunctions.These specifications can express safety properties over a conjunction of polyhedra.Source: E. Complexity · p. 6
  • For SNN-STL with linear predicates, convexity of the optimization problem without STL constraints implies convexity after adding the STL constraints, yielding polynomial-time synthesis.The resulting problem can be encoded as an LP without integer variables.Source: E. Complexity · p. 6

V. MODEL PREDICTIVE CONTROL SYNTHESIS

The MPC synthesis approach repeatedly plans over finite horizons while retaining the history needed to enforce STL specifications. For specified unbounded formulas, it extends this process to an infinite sequence, with correctness depending on exact disturbance predictions.

A. Synthesis for bounded-time STL formulas

  • For bounded-time formulas, the horizon H is at least the formula bound; MPC executes only the first computed input and then replans while retaining past states and inputs.The retained history supports enforcing the formula over the length-H trajectory prefix.Source: A. Synthesis for bounded-time STL… · pp. 6–7

B. Extension to unbounded formulas

  • For safety formulas of the form □ϕ_MPC, where ϕ_MPC has bound H, plans of length 2H are stitched together while tracking past values and robustness constraints.The method omits loop constraints because it searches finite trajectories rather than an infinite trajectory with a finite parametrization.Source: B. Extension to unbounded formulas · p. 7
  • If Algorithm 2 does not terminate, its repeatedly generated inputs satisfy □ϕ_MPC; the approach also applies to bounded-time ϕ_MPC and ϕ_MPC U ψ_MPC formulas.The extension assumes exact predictions of disturbances over the next 2H steps.Source: B. Extension to unbounded formulas · pp. 7–8
  • The control objective is STL satisfaction rather than closed-loop stability, achieved through choosing a sufficiently large prediction horizon H.The paper compares this horizon choice with prior use of sufficiently large horizons to attain terminal constraints.Source: B. Extension to unbounded formulas · p. 8

VI. EXPERIMENTAL COMPARISON OF ENCODINGS

The Boolean and robustness encodings were compared on constraint counts and MILP generation and solver times. The robustness encoding generated more constraints, while its overall computation time was usually less than twice that of the Boolean encoding, with a notable exception for ϕ4.

VI. EXPERIMENTAL COMPARISON OF ENCODINGS

  • The experiments compared both encodings for formulas with horizon N = 30 and sampling time τ = 0.025s, reporting constraint counts and MILP generation and solver times.The reported runs used a laptop with an Intel Core i7 2.3 GHz processor and 16 GB of memory.Source: §VI · p. 8
  • Most computation time was spent creating the MILP, while solving it took a fraction of a second for both encodings.Solving the robust encoding for ϕ4 took significantly longer than solving its Boolean encoding; the reason was unclear without further investigation.Source: §VI · p. 8
  • The robust encoding generates 3 to 5 times more constraints than the Boolean encoding, while creating and solving the corresponding MILPs takes hardly twice as long; solving ϕ4 is an exception.Source: §VI · p. 8

VII. CASE STUDY: BUILDING CLIMATE CONTROL

The building is modeled as a resistor-capacitor network of rooms and walls, with heat-transfer dynamics governing temperatures under HVAC inputs and disturbances.

A. Mathematical Model of a Building

  • The building model represents n nodes, including m rooms and n − m walls, as a resistor-capacitor network.Room and wall temperatures are modeled as state variables.Source: A. Mathematical Model of a Building · pp. 8–9
  • The thermal model represents wall and room heat transfer using parameters such as heat capacity, thermal resistance, radiation, and neighboring-node interactions.Source: A. Mathematical Model of a Building · p. 8
  • Heat-transfer equations for the walls and rooms define the system dynamics, written as ẋ_t = f(x_t, u_t, w_t).Source: A. Mathematical Model of a Building · p. 9
  • The input includes air mass flow and supply-air temperature, but the studied HVAC system keeps supply temperature constant and varies air mass flow.The disturbance vector aggregates unmodelled effects, including outdoor temperature and internal and radiative heat, estimated from historical data.Source: A. Mathematical Model of a Building · p. 9

B. MPC for Building Climate Control

The case studies apply MPC to building climate control and power-system regulation, using STL constraints to express desired behavior while optimizing control inputs.

B. MPC for Building Climate Control

A. Mathematical Model

  • Area Control Error combines frequency and tie-line deviations, and its integral contributes to the auxiliary feedback signal.Source: A. Mathematical Model · p. 10
  • The smart-grid model treats demand variation as a disturbance and ancillary power as a control input that complements primary AGC.The power-system model includes interconnected areas with governor, turbine, and generator dynamics.Source: A. Mathematical Model · pp. 9–10

B. MPC for Ancillary Services

The ancillary-services controller uses STL constraints in MPC to regulate Area Control Error while limiting ancillary inputs and optimizing their use.

B. MPC for Ancillary Services

IX. RELATED WORK

The paper extends bounded-model-checking-style synthesis to full STL through mixed-integer linear encodings, building on prior temporal-logic control work with narrower specifications or potentially expensive automata operations. Its conclusion reports smart-grid and HVAC demonstrations and identifies uncertain environments and arbitrary unbounded STL properties as future directions.

IX. RELATED WORK

  • Earlier receding-horizon methods address GR(1) or synthetically co-safe LTL, while full-LTL automata methods may require finite-state abstraction and a Büchi automaton.The paper instead uses bounded model checking to avoid those potentially expensive operations.Source: §IX · p. 11
  • The work extends bounded model checking to full STL for continuous systems, whose specifications can express safety, liveness, and response properties.Source: §IX · p. 11

X. CONCLUDING REMARKS

  • A pair of bounded-model-checking-style encodings turns STL specifications into mixed-integer linear constraints for feasible and optimal controller synthesis, including maximum robustness of satisfaction.The formulation can be used within existing controller-synthesis frameworks.Source: §X · p. 11
  • Experiments use simplified smart-microgrid and HVAC models, with simulations illustrating the effectiveness of the proposed MPC schemes.Source: §X · p. 11
  • Reactive synthesis for uncertain environments and synthesis for arbitrary unbounded STL properties are identified as future work.The authors describe unbounded STL as an easy extension for certain property types, while arbitrary properties require further exploration.Source: §X · p. 11
Loading 1703.09563v1…