Source-linked AI summary
A Smooth Robustness Measure of Signal Temporal Logic for Symbolic Control
Yann Gilpin, Vince Kurtz, Hai Lin
TL;DR
STL robust semantics make trajectory synthesis an optimization problem, but exact MIP methods scale poorly and existing smooth approximations trade off soundness and completeness. This paper proposes a smooth robustness measure that is sound and asymptotically complete, with tunable conservativeness. Simulations show it can find a satisfying path through a narrow passage and scales roughly linearly with specification complexity and length, unlike exponential MIP methods.
Problem
Exact MIP-based STL synthesis scales poorly, while smooth robustness approximations can sacrifice soundness or completeness.
Source: §I · p. 1Method
The paper replaces robustness min and max operations with smooth approximations that combine soundness and asymptotic completeness with a tunable conservativeness tradeoff.
Source: §I · pp. 1–2, §III · p. 3, B. Optimization and Smooth… · p. 3Results
The proposed measure found a satisfying path through a narrow tunnel where AGM did not, and its runtime scaled roughly linearly with specification complexity and length while MIP scaled exponentially.
Source: §IV · pp. 5–6Takeaways & Limitations
Parameter choice lets users favor closeness to true robustness at larger values or more conservative behavior at smaller values.
Source: B. Optimization and Smooth… · p. 3, §V · p. 6
Abstract
from arXiv · showhide
Recent years have seen an increasing use of Signal Temporal Logic (STL) as a formal specification language for symbolic control, due to its expressiveness and closeness to natural language. Furthermore, STL specifications can be encoded as cost functions using STL's robust semantics, transforming the synthesis problem into an optimization problem. Unfortunately, these cost functions are non-smooth and non-convex, and exact solutions using mixed-integer programming do not scale well. Recent work has focused on using smooth approximations of robustness, which enable faster gradient-based methods to find local maxima, at the expense of soundness and/or completeness. We propose a novel robustness approximation that is smooth everywhere, sound, and asymptotically complete. Our approach combines the benefits of existing approximations, while enabling an explicit tradeoff between conservativeness and completeness.
I. INTRODUCTION
STL robust semantics turn trajectory synthesis into optimization, but exact MIP methods scale poorly and smooth approximations trade off soundness, completeness, and conservativeness. The proposed approximation combines smoothness and soundness with asymptotic completeness and an explicit conservativeness tradeoff.
I. INTRODUCTION
- STL robust semantics maps a signal to a scalar that is positive only when the specification is satisfied, making synthesis an optimization over control sequences.The symbolic control problem is to design a trajectory satisfying the specification.Source: §I · p. 1
- MIP can solve the robustness optimization exactly, but scales poorly with system dimension, trajectory length, and specification complexity.Each predicate at each timestep adds an integer variable, and MIP complexity is exponential in their number.Source: §I · p. 1
- Smooth robustness approximations enable faster gradient-based optimization and improve scalability over MIP, but may find only local maxima unless the specification is convex.The optimization remains non-convex in general.Source: §I · p. 1
- LSE robustness is smooth and asymptotically complete, whereas AGM robustness is sound and more conservative but not smooth everywhere.LSE may overapproximate true robustness; AGM's conservativeness tends to increase robustness to disturbances.Source: §I · p. 1
- The proposed approximation is smooth everywhere, sound, asymptotically complete, and tunable for an explicit tradeoff between conservativeness and completeness.Its under-approximation can be made more conservative, while larger parameter values bring it closer to true robustness.Source: §I · pp. 1–2
II. BACKGROUND
The paper considers nonlinear discrete-time systems whose states, control inputs, and output signals evolve according to specified dynamics. The control objective is to find an input sequence producing an output that satisfies a bounded-time STL specification.
II. BACKGROUND
- The system model maps state and control input to the next state and output at each discrete timestep.The dynamics are given by functions f and g.Source: §II · p. 2
- The synthesis goal is to choose a control sequence from an initial condition so the resulting output satisfies a bounded-time STL specification.Source: §II · p. 2
- The system functions f and g are assumed continuous and locally Lipschitz.Source: §II · p. 2
A. STL Robust Semantics
STL formulas combine predicates with Boolean and temporal operators over signals. Robust semantics assign each signal and formula a scalar whose positivity indicates satisfaction.
A. STL Robust Semantics
- STL syntax builds formulas from predicates using negation, conjunction, and bounded until.Disjunction, implication, eventually, and always can be derived from these operators.Source: A. STL Robust Semantics · p. 2
- A predicate is defined by a function of the output signal, and the paper restricts formulas to bounded time with a finite upper bound.Source: A. STL Robust Semantics · p. 2
- Robust semantics associate a scalar robustness measure with a signal, and the specification is satisfied if and only if that value is positive.Source: A. STL Robust Semantics · p. 2
B. Optimization and Smooth Approximations
STL robust semantics convert synthesis into an optimization over control sequences, but the resulting problem is generally non-smooth and non-convex. Smooth approximations support gradient-based optimization while differing in soundness, completeness, and conservativeness.
B. Optimization and Smooth Approximations
- The control sequence is optimized to maximize STL robustness, with positive robustness indicating a satisfying output.Source: B. Optimization and Smooth… · p. 2
- MIP formulations have exponential complexity in the number of predicates and timesteps, limiting their use for high-dimensional systems, complex specifications, and long tasks.Source: B. Optimization and Smooth… · p. 2
- LSE robustness is smooth and asymptotically complete, but finite-parameter overapproximation means positive LSE robustness does not guarantee satisfaction.Gradient-based methods can find local maxima, but the optimization remains non-convex.Source: B. Optimization and Smooth… · pp. 2–3
- AGM robustness is a sound under-approximation whose added conservativeness can improve disturbance and modeling-error robustness, but its gradient is undefined everywhere.This prevents a guarantee of convergence to a local maximum using gradient-based optimization.Source: B. Optimization and Smooth… · p. 3
- The proposed smooth measure is sound and asymptotically complete, with parameters that trade greater conservativeness against closeness to true robustness.Large parameter values approach true robustness; smaller values produce a significant under-approximation and more conservative behavior.Source: B. Optimization and Smooth… · p. 3
III. PROPOSED SMOOTH ROBUSTNESS
The proposed smooth robustness measure replaces minimum and maximum operators with a pair of approximations to obtain a smooth robustness function.
III. PROPOSED SMOOTH ROBUSTNESS
- Replacing instances of minimum and maximum with a pair of approximations yields a smooth approximation of the robustness function.The measure is defined through separate approximations for maximum and minimum.Source: §III · p. 3
A. Several Smooth Approximations
The section develops smooth approximations for minimum and maximum, with properties that support optimization and sound robustness assessment.
A. Several Smooth Approximations
- The smooth minimum uses a log-sum-exponential approximation and under-approximates the true minimum for k1 > 0.Its least accuracy occurs when all input arguments are equal.Source: A. Several Smooth Approximations · p. 3
- In this paper, soundness means positive robustness implies satisfaction, while completeness means the converse.The paper notes that its terminology differs from that in.Source: A. Several Smooth Approximations · p. 3
- For k2 > 0, the smooth maximum under-approximates the true maximum and approaches it as k2 increases.The approximation also has a well-defined gradient.Source: A. Several Smooth Approximations · pp. 3–4
- A positive value of the smooth robustness measure guarantees satisfaction, and the approximation has a well-defined gradient.The under-approximation of maximum supports the satisfaction guarantee.Source: A. Several Smooth Approximations · p. 4
- At k2 = 0, the smooth maximum is the arithmetic mean of its input vector.The remark identifies a connection between this maximum approximation and AGM robustness.Source: A. Several Smooth Approximations · p. 4
B. Smooth Robustness
The paper defines smooth STL robustness by substituting smooth minimum and maximum approximations into the robustness semantics. The resulting measure is sound and asymptotically complete, with parameter choices governing its conservativeness.
B. Smooth Robustness
- Substituting smooth minimum and maximum approximations into the robustness semantics defines the smooth robustness measure.The formulation assumes disjunctive normal form and introduces the release operator; any STL formula can be rewritten in that form with linear length.Source: B. Smooth Robustness · p. 4
- At finite parameter values, positive smooth robustness is sufficient for satisfaction, but necessary only in the limit as k1 and k2 tend to infinity.Thus, nonpositive smooth robustness at finite parameter values does not rule out satisfaction.Source: B. Smooth Robustness · p. 4
- If the smooth robustness is positive, the signal satisfies the bounded-time STL specification.The result is stated for any discrete-time signal and bounded-time specification.Source: B. Smooth Robustness · p. 4
- For any finite STL specification and discrete-time signal, sufficiently large k1 and k2 make smooth robustness arbitrarily close to true robustness.The paper states that sufficiently large parameters prevent the approximation from hiding potential solutions.Source: B. Smooth Robustness · pp. 4–5
- Low parameter values replicate averaging behavior, while high values approach true robustness and mimic LSE's asymptotic completeness.The figure contrasts low- and high-parameter cases.Source: Figure 1 · p. 5, B. Smooth Robustness · p. 5
IV. SIMULATION RESULTS
The simulations compare the proposed smooth robustness measure with existing approaches and test its behavior in path-planning and scalability scenarios. They report higher traditional robustness scores than the alternatives and roughly linear scaling in the tested variables.
IV. SIMULATION RESULTS
- For small k1 and k2, the trajectories showed averaging behavior, arriving quickly at targets and staying as long as possible to improve disturbance robustness.The passage relates this conservative behavior to robustness against external disturbances.Source: §IV · p. 5
- With large k1 and k2, the proposed measure closely approximated true robustness and enabled a satisfying path through a narrow tunnel where AGM found none.The passage notes that an overly conservative measure would be unable to find a satisfying path through the tunnel.Source: §IV · p. 5
- Apparent obstacle clipping is a time-discretization artifact that can be resolved with a smaller sampling period or inflated obstacles.The note applies to the plotted trajectories.Source: §IV · p. 5
- The proposed approach achieved higher average traditional robustness (¯ρ) and lower standard deviation (σρ), with computation similar to LSE and slower than AGM.Optimization times are not directly comparable because AGM used MATLAB and fmincon, while EF and LSE used Python and scipy’s SQP method.Source: Table II · p. 5, §IV · p. 5
- Runtime scaled roughly linearly with charging-station count (P) and timestep count (N), whereas MIP-based methods scale exponentially in both.The results average more than 100 runs with random initial states.Source: Figure 3 · p. 6, §IV · p. 6
V. CONCLUSION
The paper concludes that its new smooth STL robustness measure is sound and asymptotically complete. It combines benefits of existing approximations while allowing conservativeness and completeness to be traded off.
V. CONCLUSION
- The proposed smooth robustness measure is sound—a positive value is sufficient for satisfaction—and asymptotically complete, meaning it can approach true robustness arbitrarily closely.These properties combine benefits of existing smooth approximations.Source: §V · p. 6
- The measure enables an explicit tradeoff between conservativeness and completeness.The paper identifies developing efficient optimization techniques that exploit the measure’s structure as future work.Source: §V · p. 6
- Future work will develop efficient optimization techniques that exploit the measure’s structure to find satisfying trajectories more effectively.Source: §V · p. 6