PaperlayerView exact revision on arXiv

Source-linked AI summary

Arithmetic-Geometric Mean Robustness for Control from Signal Temporal Logic Specifications

Noushin Mehdipour, Cristian-Ioan Vasile, Calin Belta

arXiv:1903.05186v1cs.RO

TL;DR

Traditional STL robustness emphasizes the most critical satisfaction or violation rather than satisfaction across subformulae and time points. The paper proposes AGM robustness and uses it in control synthesis. In disturbance simulations, the AGM-maximizing policy has a lower reported failure rate than the approximation-robustness-maximizing policy.

  • Problem

    Traditional robustness reflects the most critical satisfaction or violation, while the paper seeks a score that accounts for satisfaction across subformulae and time points.

    Source: §I · p. 1, §VII · p. 8

  • Method

    The paper defines normalized AGM robustness using arithmetic and geometric means and uses gradient ascent to maximize it in STL-constrained control.

    Source: §III · p. 2, §IV · p. 3, §V · p. 6

  • Results

    The disturbed policy maximizing approximation robustness fails to satisfy the specification 58% of the time, while the policy maximizing AGM robustness has an average failure rate of 41%.

    Source: C. Performance Under Disturbance · p. 8

  • Takeaways & Limitations

    The authors report that AGM robustness provides a better satisfaction or violation score in monitoring and control, with better average performance under external disturbance than traditional robustness.

    Source: §VII · p. 8

Abstract

from arXiv · show

We present a new average-based robustness score for Signal Temporal Logic (STL) and a framework for optimal control of a dynamical system under STL constraints. By averaging the scores of different specifications or subformulae at different time points, our new definition highlights the frequency of satisfaction, as well as how robustly each specification is satisfied at each time point. We show that this definition provides a better score for how well a specification is satisfied. Its usefulness in monitoring and control synthesis problems is illustrated through case studies.

I. INTRODUCTION

STL quantifies how well system executions satisfy temporal requirements, but traditional robustness focuses on the most critical subformula or time point. The paper introduces AGM robustness to account for satisfaction across subformulae and time points.

I. INTRODUCTION

  • MILP-based STL control can fail to scale with many variables or complex temporal constraints, and nonlinear dynamics require linearization when possible.Heuristic methods avoid smoothness requirements but do not guarantee finding optima and require user-set parameters.Source: §I · p. 1
  • Smooth robustness approximations address non-differentiability but can misclassify satisfaction unless robustness exceeds a predefined threshold.Earlier average-based approaches focused on temporal operators while retaining traditional max/min functions for other operators.Source: §I · p. 1
  • AGM robustness uses arithmetic and geometric means across subformulae and relevant time points, rewarding satisfaction at more time steps and with higher scores.The paper reports a better satisfaction margin under disturbances and a normalized signed score for comparing specifications on differently scaled signals.Source: §I · pp. 1–2

A. Signal Temporal Logics (STL)

  • STL describes temporal properties of real-valued signals using predicates combined with Boolean and temporal operators, including eventually and always.Its quantitative semantics, or robustness, measures how much a signal satisfies or violates a specification.Source: A. Signal Temporal Logics (STL) · p. 2
  • Traditional STL robustness is sound: positive scores imply satisfaction, while negative scores imply violation.Its recursive definition uses min and max operators, which are non-differentiable.Source: A. Signal Temporal Logics (STL) · p. 2, B. min/max Approximation · p. 2

III. PROBLEM STATEMENT

The control synthesis problem is to choose inputs for a discrete-time dynamical system so its trajectory satisfies an STL specification while optimizing cost. The paper frames its approach around addressing the limitations of robustness scores that emphasize only the most satisfying or violating part.

III. PROBLEM STATEMENT

  • Control synthesis chooses a finite-horizon control policy whose generated trajectory satisfies an STL specification while optimizing cost.The system evolves through state updates determined by its dynamics and control inputs.Source: §III · p. 2
  • The traditional robustness score considers only the most satisfying or violating part of a specification, overlooking its other parts.Prior solutions include heuristic algorithms, MILP encoding, and gradient ascent.Source: §III · p. 3

IV. ARITHMETIC-GEOMETRIC MEAN (AGM) ROBUSTNESS

AGM robustness replaces traditional max/min aggregation with arithmetic and geometric means over subformulae and relevant time points, yielding a normalized signed score whose sign indicates satisfaction or violation.

  • AGM robustness uses a normalized signed score: positive values indicate satisfaction, negative values indicate violation, and zero indicates inconclusiveness.The score lies in [-1,1], and its absolute value measures how well the specification is satisfied or violated.Source: §IV · p. 3
  • The definition assumes bounded signals whose components are normalized to [-1,1], and recursively combines robustness values across Boolean and temporal operators.The algorithms determine satisfaction or violation and the resulting score from individual subformula robustness values.Source: §IV · p. 3
  • The ANY command checks satisfaction or violation and determines the resulting score, with worst-case complexity O(n).Source: §IV · p. 3
  • AGM robustness is sound: a satisfying trajectory has strictly positive robustness, with the sign distinguishing satisfaction from violation.The proof proceeds by structural induction over the formula.Source: §IV · p. 3

A. Logic properties

The section defines AGM conjunction, disjunction, negation, and implication operations, then establishes their logical properties, including a Kleene algebra condition despite failure of distributivity.

A. Logic properties

  • The conjunction and disjunction functions satisfy idempotence, while negation is defined as n(x) = -x and implication as ▽(-x,y).The paper also notes weaker absorption conditions for conjunction and disjunction.Source: A. Logic properties · pp. 3–4
  • AGM operations satisfy non-contradiction, excluded middle, DeMorgan’s law, double negation, and modus ponens.Source: A. Logic properties · p. 4
  • Although the AGM operations do not form a distributive lattice, they satisfy the Kleene algebra condition.Source: A. Logic properties · p. 4

B. Performance Properties

AGM robustness is smooth almost everywhere with a nonzero gradient wherever smooth, and its arithmetic/geometric aggregation distinguishes satisfaction levels that traditional max/min scores can tie. It also provides a better satisfaction margin under disturbance.

B. Performance Properties

  • AGM robustness is smooth almost everywhere except at satisfaction boundaries, and its gradient is nonzero wherever it is smooth.The stated boundaries are where a subformula’s traditional robustness equals zero.Source: B. Performance Properties · p. 4
  • Arithmetic and geometric means account for robustness across subformulae and relevant times, rather than only the most critical satisfaction or violation.Source: B. Performance Properties · p. 4
  • For F[1,4](S > 0.5), traditional robustness is 0.5 for all three signals, while AGM scores are 0.5, 0.25, and 0.125 for S1, S2, and S3.For G[0,4](S > 0.5), traditional scores are 0.5 for S1 and 0.1 for S2 and S3, while AGM scores are 0.5, 0.41, and 0.1, respectively.Source: Figure 1 · p. 5, B. Performance Properties · p. 5
  • For φ3 = F[1,4](S > 0.9), a disturbance greater than 0.1 at t = 1 violates the specification for S3, while S1 remains satisfying under the same disturbance.Both signals have the same stated traditional and AGM score of 0.1 in the comparison.Source: B. Performance Properties · p. 5

C. Normalization

Normalization makes robustness comparisons meaningful when predicates use variables with different ranges; the paper illustrates this with robot position and battery level.

C. Normalization

  • Without normalization, the position predicate has robustness 1 while the battery predicate has robustness 50, making the conjunction score 1 across battery values 31–100 despite differing variable scales.The paper describes normalization as essential in practice for interpreting satisfaction across such differently scaled properties.Source: C. Normalization · p. 5

V. CONTROL USING THE AGM ROBUSTNESS

The control framework maximizes AGM robustness to find trajectories with strong satisfaction margins, optionally balancing robustness against control cost. For smooth dynamics, it uses gradient-based optimization of the control sequence.

V. CONTROL USING THE AGM ROBUSTNESS

  • A positive robustness score provides a margin within which perturbations up to that score do not change specification satisfaction.The framework maximizes robustness to seek the strongest-satisfying trajectory, not merely any satisfying one.Source: §V · pp. 5–6
  • For smooth system dynamics, gradient ascent can maximize AGM robustness instead of relying on heuristic methods or MILP encoding.The optimization starts from a random control sequence and updates it to maximize AGM robustness for the system execution.Source: §V · p. 6
  • Because AGM robustness is nonsmooth at satisfaction boundaries, the method uses proximal stochastic gradient ascent or sub-gradient ascent with diminishing step size.The step size is the gradient method’s tuning parameter described here.Source: §V · p. 6
  • The combined fitness function balances maximizing robustness and minimizing control cost, with λ setting the trade-off.Assuming the cost function is smooth, a similar gradient-ascent optimization can solve the constrained nonlinear problem.Source: §V · p. 6

VI. CASE STUDIES

The case studies examine control synthesis for linear and nonlinear systems, with and without disturbance, and compare AGM-based results with MILP and smooth-approximation approaches.

VI. CASE STUDIES

  • The case studies cover control synthesis in linear and nonlinear systems, both with and without external disturbance.The comparisons use MILP for traditional robustness and SQP for approximation robustness.Source: §VI · p. 6
  • The experiments set λ = 0 to emphasize differences among AGM, traditional, and approximation robustness.Gradient-ascent simulations use MATLAB; MILP uses Gurobi in Python.Source: §VI · p. 6
  • Gradient ascent is capped at 300 iterations in the reported simulations.Source: §VI · p. 6

A. AGM Robustness Versus Traditional Robustness

In the nonholonomic robot case, AGM robustness favors trajectories that satisfy subformulae over more time points, unlike traditional robustness, which rewards peak satisfaction at critical points. The MILP comparison requires linearizing the dynamics.

A. AGM Robustness Versus Traditional Robustness

  • The test task requires remaining in the initial region for five steps, visiting Reg1 and Reg2 in sequence, and always avoiding an obstacle.The robot starts at q0 = [0.5,5,0], with bounded position, orientation, and control inputs.Source: A. AGM Robustness Versus Traditional… · p. 6
  • The MILP baseline uses feedback linearization, so position is controlled directly while orientation is controlled indirectly.For φ1 with horizon T = 15, the encoding has 95 continuous and 70 binary variables; the passage cautions that MILP does not scale well to complex specifications or long horizons.Source: A. AGM Robustness Versus Traditional… · p. 6
  • Traditional robustness reaches the same maximum ρ = 1 for two trajectories, while AGM rewards earlier, longer region visits and satisfaction across subformulae.The AGM-selected trajectory visits Reg1 at t = 9 and 10, aims toward region centers, and avoids the obstacle.Source: A. AGM Robustness Versus Traditional… · p. 6, Figure 2 · p. 7

B. AGM Robustness Versus Approximation Robustness

Across the approximation-robustness and disturbance case studies, AGM favors satisfaction across more time points and performs better under added noise. The reported comparisons contrast AGM with smooth approximation and traditional robustness.

B. AGM Robustness Versus Approximation Robustness

  • For φ2, the approximation-selected trajectory visits Reg1 at t = 4 and Reg3 at t = 10 once, while AGM visits Reg1 at t = 3,4 and Reg3 at t = 8,9,10.Both approaches generate satisfying trajectories; AGM also directs the trajectory toward region centers while maintaining distance |η| from the obstacle.Source: B. AGM Robustness Versus Approximation… · p. 7
  • The paper identifies approximation error from soft maximum and minimum functions as a source of differences between approximation and traditional robustness values for the same trajectory.The comparison frames AGM as removing these approximation errors and improving satisfaction performance.Source: B. AGM Robustness Versus Approximation… · p. 7

C. Performance Under Disturbance

  • For φ3 without disturbance, the approximation-robustness trajectory visits each region center once, while AGM visits Reg1 at t = 3,4 and Reg2 at t = 7,8,9.The task requires sequential visits to Reg1 and Reg2.Source: C. Performance Under Disturbance · pp. 7–8
  • The disturbance study adds Gaussian noise to previously optimized control policies and evaluates the resulting trajectories across different noise levels.Source: C. Performance Under Disturbance · p. 8
  • Under disturbance across 100 simulations, the approximation-robustness policy fails to satisfy φ3 in 58% of runs, versus an average 41% failure for the AGM policy.The reported AGM-controlled example remains satisfying, though at different time points and with a smaller robustness score.Source: C. Performance Under Disturbance · p. 8

VII. CONCLUSION AND FUTURE WORK

AGM robustness considers all appropriate subformulae and time points, rather than only critical ones. The authors report better satisfaction or violation scoring in monitoring and control, and better average performance under external disturbance when maximizing AGM robustness.

  • AGM robustness considers all subformulae at appropriate time points, not only critical subformulae or time points.Source: §VII · p. 8
  • The authors report better satisfaction or violation scores with AGM robustness than traditional robustness in monitoring and control problems.Source: §VII · p. 8
  • Under external disturbance, the system has better average performance when maximizing AGM robustness rather than traditional robustness.Source: §VII · p. 8

Related papers

Loading 1903.05186v1…