PaperlayerView exact revision on arXiv

Source-linked AI summary

Backpropagation through Signal Temporal Logic Specifications: Infusing Logical Structure into Gradient-Based Methods

Karen Leung, Nikos Aréchiga, Marco Pavone

arXiv:2008.00097v3eess.SYcs.CLcs.LO

TL;DR

Robotics needs ways to encode spatio-temporal rules in methods that operate on continuous systems and gradients, while traditional LTL is incompatible with gradient-based methods. The paper introduces stlcg, which translates STL robustness formulas into computation graphs and uses automatic differentiation to backpropagate through them. Examples across robotics applications demonstrate incorporation of logical structure and human-domain knowledge into gradient-based problem formulations.

  • Problem

    LTL specifications operate on discrete states and are incompatible with gradient-based methods, while incorporating STL can require new algorithms or added computational complexity.

  • Method

    stlcg systematically translates STL robustness formulas into computation graphs so off-the-shelf automatic differentiation tools can backpropagate through them.

  • Results

    The paper demonstrates stlcg across motion planning, behavior clustering, model fitting, intent prediction, and generative modeling examples.

  • Takeaways & Limitations

    STLCG provides a versatile way to infuse logical structure and human-domain knowledge into robotics problems that use gradient-based solution methods.

  • Takeaways & Limitations

    Smooth max/min approximations may be needed because recursive max/min operations can produce many zero gradients and numerical difficulties.

Abstract

from arXiv · show

This paper presents a technique, named STLCG, to compute the quantitative semantics of Signal Temporal Logic (STL) formulas using computation graphs. STLCG provides a platform which enables the incorporation of logical specifications into robotics problems that benefit from gradient-based solutions. Specifically, STL is a powerful and expressive formal language that can specify spatial and temporal properties of signals generated by both continuous and hybrid systems. The quantitative semantics of STL provide a robustness metric, i.e., how much a signal satisfies or violates an STL specification. In this work, we devise a systematic methodology for translating STL robustness formulas into computation graphs. With this representation, and by leveraging off-the-shelf automatic differentiation tools, we are able to efficiently backpropagate through STL robustness formulas and hence enable a natural and easy-to-use integration of STL specifications with many gradient-based approaches used in robotics. Through a number of examples stemming from various robotics applications, we demonstrate that STLCG is versatile, computationally efficient, and capable of incorporating human-domain knowledge into the problem formulation.

1 Introduction

Robotics systems operate under spatial and temporal rules, but discrete LTL specifications are poorly suited to continuous, gradient-based methods. The paper introduces stlcg, which translates STL robustness formulas into computation graphs for easier integration with existing gradient-based techniques.

  • Limitations of LTL: LTL is limited for high-dimensional, continuous, or nonlinear systems because it operates on discrete states and is incompatible with gradient-based methods.Although LTL supports automaton-based synthesis, these properties restrict its use in the targeted robotics settings.
  • Motivation: STL expresses constraints over dense-time real-valued signals and provides quantitative robustness values measuring satisfaction or violation.This makes STL applicable to trajectories from continuous dynamical systems and compatible with gradient-based methods.
  • Contribution: The paper proposes stlcg, a framework that translates any STL robustness formula into computation graphs underlying automatic differentiation.The design aims to add logical structure without significantly changing existing algorithmic and computational foundations.
  • Contributions: The revised paper adds pedagogical STL material, complete computation-graph details including Until, a motion-planning example, parametric experiments, and a latent-space example.These additions extend the preliminary WAFR version.

2 Preliminaries

The preliminaries define STL over sampled real-valued signals, its recursive syntax and temporal semantics, and quantitative robustness. STL formulas are also represented by parse trees that expose their compositional structure.

  • 2.1 Signals: STL signals are finite, uniformly sampled sequences of real-valued states and associated times, with subsignals defined as contiguous fragments.The paper assumes uniform sampling interval Δt.
  • 2.2 Signal Temporal Logic: Syntax and Semantics: STL formulas are recursively built from true, differentiable predicates, negation, conjunction, and bounded Until, with other operators derived from this grammar.Eventually is represented using Until, while Always is defined through negated Eventually.
  • 2.2 Signal Temporal Logic: Syntax and Semantics: Eventually requires a subformula to hold at some time in an interval, Always requires it throughout the interval, and Until requires one formula before another becomes true.These temporal operators determine how STL evaluates signals over bounded time windows.
  • 2.2 Signal Temporal Logic: Syntax and Semantics: Quantitative STL semantics assign robustness values whose sign indicates satisfaction or violation, while conjunction and disjunction use minimum and maximum robustness, respectively.Robustness formulas provide a quantitative degree rather than only a Boolean truth value.
  • 2.2 Signal Temporal Logic: Syntax and Semantics: A robustness trace collects the robustness of a formula over every subsignal of an input signal, and Example 2 visualizes traces for Eventually, Always, and Until formulas.Figure 1 uses blue input signals and orange robustness traces for ψ1, ψ2, and ψ1 U ψ2.
  • 2.3 Graphical Structure of STL Formulas: An STL parse tree represents the formula’s recursive syntax, with operator nodes connected to subformulas and predicates or true as leaves.This structure exposes each operation making up the formula.

3 STL Robustness Formulas as Computation Graphs

STLCG systematically translates STL robustness formulas into computation graphs, implemented with a toolbox that visualizes their signal, parameter, and operation structure.

  • STLCG translates STL robustness formulas into computation graphs and combines operator-specific graphs to compute robustness traces.The framework is implemented in PyTorch and includes a graph visualizer for formula dependencies.
  • Figure 2 maps an STL formula from parse tree to computation graph, with blue signal nodes, green predicate parameters, and orange STL operations.
  • Figure 3 illustrates the analogous computation-graph representation for the operation z = w(x + y).

3.1 Computation Graphs and Backpropagation

Computation graphs expose nested operations so automatic differentiation can backpropagate derivatives through STL robustness computations.

  • A computation graph represents variables and operations as connected nodes whose outputs feed subsequent computations.For z = w(x + y), x, y, and w are inputs, + and × are operations, and z is the output.
  • Backpropagation applies the chain rule across graph edges to obtain an output derivative with respect to any dependent input.Nested functions require derivatives for each suboperation, which are multiplied along connected paths.
  • Figure 4 visualizes the backpropagation example for z = w(x + y).
  • The example assigns x = 1, y = 2, and w = 3, producing intermediate values z(1) = 3 and z(2) = 9.

3.2 Computation Graphs of STL Operators

STLCG represents non-temporal STL operators with basic mathematical graphs and temporal operators with recurrent computation graphs that exploit dynamic programming.

  • Non-temporal STL operators use computation graphs built from subtraction, max, and min operations, while temporal operators require recurrent graph structures.The recurrent structure addresses efficient computation of robustness traces over time.
  • 3.2.2 Temporal STL Operators: Eventually and Always graphs process robustness traces through recurrent hidden states, using max for Eventually and min for Always.The hidden state summarizes relevant signal values while outputs are generated through dynamic-programming updates.
  • 3.2.2 Temporal STL Operators: Eventually computation handles interval variants by shifting stored trace values and aggregating the values relevant to each temporal window.The construction uses matrices that remove the first stored element, shift entries, and insert the current input.
  • 3.2.2 Temporal STL Operators: The output states of the Eventually graph form the robustness trace, with the final recurrent output yielding the formula’s robustness value.
  • 3.2.3 Eventually and Always Operators: Figure 5 depicts predicate and logical-operator graphs, while Figure 6 shows unrolled recurrent graphs for Eventually and Always.
  • 3.2.3 Eventually and Always Operators: Eventually and Always robustness traces can be computed in O(T) time through one pass over the signal.Example 4 illustrates hidden and output states for different intervals on a six-value signal.
  • 3.2.4 Until Operator: The Until graph combines Always-based computation with loops and max/min operations to compute its robustness trace.For unbounded Until, the described procedure has O(T^2) time complexity.

3.3 Calculating Robustness with Computation Graphs

STLCG composes operator graphs according to an STL formula’s parse tree, producing exact robustness traces with bounded overall computational complexity.

  • The full graph stacks operator-specific computation graphs according to the STL formula’s parse tree and maps an input signal to its robustness trace.The total time complexity is at most O(|T|T^2), where |T| is the number of parse-tree nodes and T is signal length.
  • For every STL formula and signal, the constructed graph produces the formula’s true robustness trace exactly.This property is stated as Theorem 1 and establishes correctness by construction.

3.4 Smooth Approximations to stlcg

STLCG smooths max and min operations to address zero-gradient and point-sensitivity problems in STL robustness computations. It also introduces an integral robustness formula that spreads gradients across an interval.

  • Recursive max and min operations can produce zero gradients and numerical difficulties during backpropagation.
  • Softmax/min and logsumexp provide smooth approximations whose accuracy increases with β, which can be annealed during gradient descent.As β approaches infinity, the approximation approaches the true solution; β near zero approaches the mean of the entries.
  • Pointwise max and min can make robustness overly sensitive to one signal point, especially for noisy signals, and concentrate gradients there.
  • The integral robustness formula weights signal values over [a, b] to produce a smoother robustness trace and spread gradients.Its effect is demonstrated in the motion-planning case study.

4 Case Studies: Using stlcg for Robotics Applications

The case studies evaluate STLCG across robotics applications involving logical motion-planning constraints, computational scaling, and human-domain knowledge in neural networks.

  • The case studies examine STL in motion planning, computational efficiency through parallelization and batching, and deep-learning integration of human-domain knowledge.

4.1 Motion Planning with STL Constraints

STLCG supports gradient-based motion planning with STL constraints, including temporal ordering, obstacle avoidance, speed limits, and control bounds. The examples show feasible trajectories and smoother solutions with integral robustness.

  • Motion Planning Example 1: The first motion-planning problem drives a point-mass robot from (-1, -1) to (1, 1) under 2D integrator dynamics and an STL control constraint.The control constraint is expressed as θ = □∥u∥2 ≤ umax.
  • Motion Planning Example 1: The optimization combines linear dynamics and endpoint constraints with a ReLU penalty that encourages STL robustness to exceed margin m.The concatenated state-control vector is z = (X, U), and the dynamics are expressed as Ez = D.
  • Motion Planning Examples: The specifications include eventual persistent-region visitation, obstacle avoidance, control limits, and an Until relation imposing temporal ordering.The Until example requires visiting region A before staying in region B while avoiding region C and respecting a speed limit.
  • Motion Planning Example 1: Integral robustness produced smoother state trajectories and control signals than Always robustness, while all cases satisfied the control bound umax = 0.8.The motion-planning solutions were obtained by standard gradient descent from a straight-line initialization that violated the STL specification.
  • Motion Planning Example 2: The obstacle penalty discourages entering the obstacle but provides no additional reward for maintaining greater distance from it.
  • Motion Planning Example 2: Gradient descent produced trajectories satisfying Until, obstacle-avoidance, and speed-limit specifications after starting from a violating trajectory.The example used T = 79, ∆t = 0.1, 500 gradient steps, and step size 0.5.

4.2 Parametric STL for Behavioral Clustering

STLCG enables parametric STL estimation across independent signals using batching, vectorization, and GPU computation. These capabilities improve scalability, while non-monotonic formulas still require gradient-based sampling and leave time-parameter optimization unresolved.

  • Parametric STL estimates unknown predicate or interval parameters to fit signals, providing a basis for time-series feature extraction and logic-based clustering.
  • Independent signals can be solved simultaneously with a combined loss, and inputs can be padded to accommodate variable signal lengths.GPU use can be added with minor code changes.
  • STLCG regularization can impose an STL requirement on neural-network outputs even when noisy training data violates that requirement.The illustrated specification requires s to remain between 0.48 and 0.52 over [1, 2.75].
  • Binary search applies to monotonic pSTL formulas, whereas non-monotonic formulas with multiple local minima require gradient descent, multiple parameter samples, and β annealing.
  • Batched or vectorized STLCG computation scales more efficiently than sequential binary search, while GPU parallelization provides near-constant computation time for larger problem sizes.Both approaches converged to the same solution in the reported comparison.
  • STLCG currently cannot optimize time parameters defining an interval because gradients cannot be backpropagated through those parameters.The authors identify this as future work.

4.3 Robustness-Aware Neural Networks

STLCG incorporates STL-based robustness into neural networks to encode known structure and desired behaviors. Across model fitting, sequence prediction, and latent-space modeling, the examples show improved adherence to specifications or coverage of expert-defined modes.

  • 4.3.1 Model Fitting with Known Structure: STLCG regularization encourages neural-network outputs to violate a known STL specification as little as possible, though it does not guarantee satisfaction.The incentive is controlled by γ through an added robustness loss.
  • 4.3.2 Sequence-to-Sequence Prediction: Short-horizon training plus STL robustness regularization enables an RNN to predict the next ten time steps while achieving a desired long-term behavior.The model uses the first ten time steps as input and predicts the next ten, with γ = 0.1 for the robustness term.
  • 4.3.3 Latent Space: STLCG encodes expert-defined trajectory modes by tying one-hot latent vectors to STL parameter values and penalizing violations of the associated formula.The latent space has three modes, with c ∈ {0.7, 0.35, 0} selected through z^⊤C.
  • 4.3.3 Latent Space: With the additional STL loss, the VAE correctly covers three distinct trajectory modes, whereas the otherwise identical model without STL loss is used as the comparison.The STL-trained model uses γ = 4 and the comparison model uses γ = 0 under the same stated training hyperparameters.

5 Future Work and Conclusions

The paper concludes that STL computation graphs can infuse logical structure into diverse robotics problems solved with gradient-based methods. It also identifies extensions to STL expressiveness, parameter optimization, and robustness of learning-based components as future directions.

  • 5 Future Work and Conclusions: STLCG transcribes STL robustness formulas into computation graphs, enabling STL specifications to be incorporated into gradient-based robotics problems.The paper demonstrates this across motion planning, behavior clustering, model fitting, intent prediction, and generative modeling.
  • 5 Future Work and Conclusions: The demonstrated applications use STL to infuse logical structure into motion planning, behavior clustering, and several learning-based robotics problems.The conclusion lists model fitting, intent prediction, and generative modeling among the learning-based applications.
  • 5 Future Work and Conclusions: Future work includes optimizing STL temporal intervals, extending the language beyond standard STL expressiveness, and studying robustness of learning-based components.These directions are presented as extensions of the theory and applications developed in the paper.
Loading 2008.00097v3…