Source-linked AI summary
Invariant Funnels around Trajectories using Sum-of-Squares Programming
Mark M. Tobenkin, Ian R. Manchester, Russ Tedrake
TL;DR
The paper addresses computing finite-time funnels around trajectories for polynomial differential equations, motivated by trajectory trees for nonlinear control. It uses SOS verification with time-varying Lyapunov functions, including an exact-condition method for approximate trajectories and a time-sampled alternative. The sampled method recovers nearly identical funnels in the reported example while computing substantially faster.
Problem
Computing finite-time invariant funnels around trajectories is motivated by nonlinear-control designs built from locally stabilized trajectory trees, where larger verified funnels support sparser trees.
Source: §1 · p. 1Method
Results
The time-sampled and exact methods produced nearly identical funnels in the satellite example, and the sampled method was substantially faster to compute.
Source: §1 · p. 1, §5.2 · p. 6Takeaways & Limitations
The reported satellite example shows that sampling in time can recover nearly identical funnels while reducing computation time.
Source: §1 · p. 1, §5 · p. 5, §5.2 · p. 6The sampled verification lacks a constructive sampling bound from computable quantities and applies its stated result only to a fixed Lyapunov function, although the optimization uses fixed sampling intervals.
Source: §4 · p. 4
Abstract
from arXiv · showhide
This paper presents numerical methods for computing regions of finite-time invariance (funnels) around solutions of polynomial differential equations. First, we present a method which exactly certifies sufficient conditions for invariance despite relying on approximate trajectories from numerical integration. Our second method relaxes the constraints of the first by sampling in time. In applications, this can recover almost identical funnels but is much faster to compute. In both cases, funnels are verified using Sum-of-Squares programming to search over a family of time-varying polynomial Lyapunov functions. Initial candidate Lyapunov functions are constructed using the linearization about the trajectory, and associated time-varying Lyapunov and Riccati differential equations. The methods are compared on stabilized trajectories of a six-state model of a satellite.
1. INTRODUCTION
The paper develops finite-time funnels to support sparse trees of locally stabilized trajectories leading to a goal point. It extends SOS verification with alternating convex optimizations and offers a faster time-sampled alternative.
1. INTRODUCTION
- Funnel size matters because larger verified regions can support sparser trees of locally stabilized trajectories leading to a goal point.The tree-based nonlinear-control motivation is attributed to Tedrake et al. (2010).Source: §1 · p. 1
- Alternating convex optimizations replace greedy nonconvex optimization, and the method can certify invariance despite using an approximate numerical trajectory.The paper also proposes time-sampled verification, which recovers almost identical funnels and is substantially faster to compute.Source: §1 · p. 1
- Unlike prior work producing outer approximations of reached sets, this method constructs inner approximations of solutions that reach a goal region.The comparison is with Julius and Pappas (2009).Source: §1 · p. 1
1.1 Notation
- The notation section defines SOS polynomials as polynomials expressible as sums of squares of polynomials.It also introduces notation for positive definite matrices and polynomial sets.Source: §1.1 · p. 1
2. PRELIMINARIES
The preliminaries define funnels into a goal region and give a Lyapunov-based condition for verifying them. Candidate functions are built around a nominal trajectory and converted to piecewise-polynomial form for SOS verification.
2. PRELIMINARIES
- A funnel into G is an invariant family of time-indexed sets whose final-time slice lies inside G, making it an inner approximation of trajectories that pass through G at the final time.The goal is to find the largest such funnel, for example by volume.Source: §2 · p. 2
- A time-varying Lyapunov function defines sublevel sets that form a funnel when its derivative satisfies the stated boundary condition; the final sublevel set must lie in G for a funnel into G.The goal region is an ellipse for the SOS relaxation, though more general polynomial goal regions are possible.Source: §2 · p. 2
2.1 A Class of Lyapunov Functions
- A Lyapunov differential equation supplies a candidate function whose unit sublevel set is a positive funnel into the goal region.The construction centers the function near a nominal solution that reaches the goal region and chooses its terminal matrix using an ellipse contained in that region.Source: §2.1 · p. 2
- A sufficiently large rescaling parameter makes the candidate's derivative negative on the level-set boundary throughout the finite time interval, yielding a nonempty funnel at every time.The initial candidate is based on the linearization around the nominal trajectory and a time-varying Lyapunov equation.Source: §2.1 · pp. 2–3
2.2 Polynomial Lyapunov Functions
- Piecewise-polynomial approximations of the trajectory and Lyapunov matrix enable SOS verification without requiring the approximate trajectory to be exact.The certificate conditions apply on the level set V(t, x) = 1, so behavior near V(t, x) = 0 is not essential.Source: §2.2 · p. 3
3. OPTIMIZATION PROCEDURE
The optimization procedure uses SOS constraints and alternating updates to improve a time-varying rescaling of a candidate Lyapunov function. It separates multiplier search from rescaling improvement to handle the bilinear constraints.
3. OPTIMIZATION PROCEDURE
- SOS constraints test polynomial negativity over semialgebraic sets, and the optimization parameterizes the Lyapunov function through the time-varying rescaling ρ(t).The formulation uses knot intervals and a linear surrogate for funnel volume.Source: §3 · p. 3
3.1 The Multiplier-Step: Finding LaGrange Multipliers
- The multiplier step fixes ρ(t) and searches for Lagrange multipliers on each interval; negative slack values certify feasibility.The interval programs can be computed in parallel, while an initial feasible ρ(t) is sought by increasing a decay parameter and, if needed, adding knot points.Source: §3.1 · pp. 3–4
3.2 The V -Step: Improving ρ(t).
- With the multipliers fixed, the V-step optimizes ρ(t); provided its function class contains the previous ρ(t), the optimization remains feasible and cannot lower the achieved objective.This alternating update addresses the bilinearity between ρ and the multipliers.Source: §3 · p. 3, §3.2 · p. 4
4. SAMPLING IN TIME
Time sampling reduces the polynomial SOS verification burden by checking the conditions at selected times, but it does not generally give an exact certificate. A partial result explains when fine sampling can expose a violation, while leaving a computable sampling bound unresolved.
4. SAMPLING IN TIME
- The degree of time in constrained polynomials is identified as the main computational bottleneck motivating time sampling.The sampled formulation chooses finer points within each interval and imposes constraints at those points.Source: §4 · p. 4
- The sampled SOS method checks the conditions only at selected times, removing algebraic dependence on time but not generally providing an exact certificate.It uses bilinear alternation to improve the initial feasible ρ(t) and the Lagrange multipliers.Source: §4 · p. 4
- Fine enough sampling can reject a fixed candidate that violates the continuous-time condition, but the result supplies no computable sampling bound and does not cover optimization over candidates.The argument relies on a violation persisting over an open time interval; the authors are studying more constructive bounds.Source: §4 · p. 4
5. NUMERICAL EXPERIMENTS
The experiments illustrate the procedure on a one-dimensional polynomial system and compare exact and time-sampled methods on a stabilized satellite trajectory.
5.1 A One-Dimensional Example
- In the one-dimensional example, a single bilinear alternation found a tight inner region, while symmetry of the Lyapunov function restricted the verified region.Additional trajectories could be used to grow the verified region; the initial and optimized sets were compared with known bounds.Source: §5.1 · p. 5
5.2 Trajectory Stabilization of Satellite Dynamics
- For satellite stabilization, the authors linearized the nominal trajectory to design a time-varying LQR controller, then used a Lyapunov function based on a piecewise-linear Riccati solution.The approximations used 49 knot points over the five-second interval.Source: §5.2 · p. 6
- The satellite example’s exact and time-sampled funnels were nearly identical, and one exact-method iteration was already good.One alternation also produced a certificate tight to known bounds, though symmetry about the trajectory makes the certificate generally suboptimal.Source: §5.2 · pp. 5–6
- The exact method used 48 multiplier SDPs, while the sampled method used 480, with 10 verification points per interval for sampling.Table 1 compares run times, but the supplied passages do not report the runtime values.Source: §5.2 · p. 6, Table 1 · p. 6
6. DISCUSSION AND FUTURE WORK
The discussion outlines implementation options and extensions to funnel verification, including broader Lyapunov-function classes and limit-cycle applications. The reported volume optimization ceases to improve after two iterations.
6. DISCUSSION AND FUTURE WORK
- Verified-funnel volume ceases to improve after two optimization iterations.Figure 2 shows successive iterations optimizing funnel volume.Source: Figure 2 · p. 6
- The paper compares optimized volumes from the exact and time-sampled methods.The discussion reports no outcome for this comparison here.Source: Figure 3 · p. 6
6.1 Sampling in Time without Splines
- Time-sampled verification need not use polynomial Lyapunov functions, allowing numerical x0(t) and P⋆0(t) instead of interpolations.Splined quantities were used in both methods only for comparison.Source: §6.1 · p. 6
6.2 Verifying Families of Funnels
- Verifying funnels across V(t, x) level sets in [a, 1] can let execution-time planning choose a funnel when the goal region is unknown beforehand.The paper gives real-time composition of preplanned trajectories as an example.Source: §6.2 · pp. 6–7
6.3 More General Lyapunov Functions
- The method is restricted to trajectory-centered rescalings of time-varying quadratic forms, a class shown to be conservative in the first numerical example.More general polynomial Lyapunov functions are possible in principle and are under investigation.Source: §6.3 · p. 7
6.4 Stability of Limit Cycles
- The authors adapted the procedure to verify regions of attraction for hybrid-system limit cycles.The cited adaptations are Manchester (2010) and Manchester et al. (2010).Source: §6.4 · p. 7