PaperlayerView exact revision on arXiv

Source-linked AI summary

Decomposition of Reachable Sets and Tubes for a Class of Nonlinear Systems

Mo Chen, Sylvia L. Herbert, Mahesh S. Vashishtha, Somil Bansal, Claire J. Tomlin

arXiv:1611.00122v3math.OC

TL;DR

High-dimensional nonlinear systems make formal reachability computationally difficult, especially when verification must handle complex dynamics and safety requirements. The paper decomposes such systems into potentially coupled lower-dimensional subsystems, enabling efficient BRS and BRT computation with substantially reduced computational burden. The method yields orders-of-magnitude speedups, while disturbances can make reconstructed sets slightly conservative.

  • Problem

    High-dimensional nonlinear, safety-critical systems require formal reachability analysis, but existing computations face severe scalability challenges.

  • Method

    The paper decomposes nonlinear dynamics into self-contained lower-dimensional subsystems that may share states, controls, and disturbances, then reconstructs full-dimensional reachable sets.

  • Results

    The method substantially reduces computation burden and enables orders-of-magnitude faster BRS and BRT computations without additional approximation errors in supported cases.

  • Takeaways & Limitations

    The decomposition makes some previously intractable high-dimensional nonlinear reachability computations tractable using compatible reachability methods.

  • Takeaways & Limitations

    In the presence of disturbances, reconstructed BRSs and BRTs can be slightly conservative approximations.

Abstract

from arXiv · show

Reachability analysis provides formal guarantees for performance and safety properties of nonlinear control systems. Here, one aims to compute the backward reachable set (BRS) or tube (BRT) -- the set of states from which the system can be driven into a target set at a particular time or within a time interval, respectively. The computational complexity of current approaches scales exponentially, making application to high-dimensional systems intractable. We propose a technique that decomposes the dynamics of a general class of nonlinear systems into subsystems which may be coupled through common states, controls, and disturbances. Despite this coupling, BRSs and BRTs can be computed efficiently using our technique without incurring additional approximation errors and without the need for linearizing dynamics or approximating sets as polytopes. Computations of BRSs and BRTs now become orders of magnitude faster, and for the first time BRSs and BRTs for many high-dimensional nonlinear control systems can be computed using the Hamilton-Jacobi (HJ) formulation. In situations involving bounded adversarial disturbances, our proposed method can obtain slightly conservative results. We demonstrate our theory by numerically computing BRSs and BRTs using the HJ formulation for several systems, including the 6D Acrobatic Quadrotor and the 10D Near-Hover Quadrotor.

I. INTRODUCTION

High-dimensional nonlinear, safety-critical systems make formal reachability difficult because verification must account for all behaviors, disturbances, continuous-time nonlinear dynamics, and large state spaces. The paper proposes decomposition-based BRS and BRT computation to reduce dimensionality while preserving supported guarantees.

  • Formal verification is needed because simulation-based approaches cannot account for all possible system behaviors.
  • Existing reachability methods trade off scalability, dynamics generality, control and disturbance handling, and set-representation flexibility.
  • The proposed method computes lower-dimensional subsystem BRSs and reconstructs the full-dimensional BRS without additional approximation errors beyond those in subsystem computations.
  • The decomposition accommodates subsystems coupled through common states, controls, and disturbances, unlike approaches requiring completely decoupled subsystems.
  • The paper develops decomposition results for both BRSs and BRTs and validates them with Hamilton-Jacobi reachability computations.
  • BRSs concern reaching a target at the end of a horizon, whereas BRTs concern reaching it at some time during that horizon.

III. PROBLEM FORMULATION

The problem formulation partitions system states into self-contained subsystems that may share common states and controls while each subsystem’s evolution depends only on its own states. This structure supports lower-dimensional reachability analysis.

  • III. PROBLEM FORMULATION: The paper seeks lower-dimensional BRS and BRT computations for systems decomposable into self-contained subsystems.
  • A. Definitions: The full state is partitioned as z = (z1, z2, zc), where zc contains states shared by both subsystems.
  • 1) Subsystem Dynamics:: Some state partitions may be independent of the control, depending on how the full dynamics depend on u.
  • 1) Subsystem Dynamics:: Subsystem states are defined as x1 = (z1, zc) and x2 = (z2, zc), allowing a finite collection of analogous subsystems.
  • 1) Subsystem Dynamics:: A self-contained subsystem has dynamics whose evolution depends only on its own state xi, not explicitly on the other subsystem.
  • 1) Subsystem Dynamics:: The subsystems can be coupled through the common state zc and a shared control u.
  • 1) Subsystem Dynamics:: The Dubins Car with constant speed v is presented as an example of a system decomposable into self-contained subsystems.

2) Projection Operators:

Projection and back-projection connect lower-dimensional subsystem sets with the full state space, enabling target-set and reachable-set reconstruction through intersections or unions. The resulting BRS and BRT conditions are established under stated subsystem assumptions.

  • 2) Projection Operators:: Projection maps a full state z = (z1, z2, zc) to its coordinates in a lower-dimensional subsystem state space.
  • 2) Projection Operators:: Back-projection lifts a subsystem point or set into a corresponding set in the full-dimensional state space.
  • 2) Projection Operators:: Fig. 2 illustrates projecting a point into the z1-zc and z2-zc planes and back-projecting subsystem sets to form their intersection in 3D.
  • 2) Projection Operators:: The full target set may be represented through intersections or unions of back-projected subsystem target sets.
  • 2) Projection Operators:: Shared variables such as zc can represent relatively complex target shapes through intersections or unions of lower-dimensional sets.
  • 2) Projection Operators:: Subsystem BRSs and BRTs are defined analogously to the full-system reachable sets using subsystem trajectories.
  • 2) Projection Operators:: The paper investigates when lower-dimensional subsystem BRSs can reconstruct the full BRS and when BRTs admit analogous decomposition.
  • 2) Projection Operators:: For self-contained systems, Theorems 1 and 2 give BRS results, while Propositions 1 and 2 provide stronger results without shared control components.

IV. SELF-CONTAINED SUBSYSTEMS

The section establishes when full-dimensional BRSs can be reconstructed from lower-dimensional subsystem BRSs, including systems coupled through shared states, controls, or disturbances. The reconstruction is exact in specified cases and follows from projection-based relationships between full and subsystem trajectories.

  • BRS decomposition: Full-dimensional BRSs can be reconstructed from lower-dimensional subsystem BRSs without additional approximation errors under the conditions of Theorems 1 and 2.The theorems apply when the full system is decomposed into self-contained subsystems.
  • BRS decomposition: A goal-state union allows reconstruction by back-projecting subsystem BRSs and combining them despite coupling between subsystems.Theorem 1 formalizes the case in which reaching either subsystem target suffices for reaching the full target.
  • Summary of cases: The section summarizes which BRS decompositions are exact or conservative for shared-state systems, with decoupled or absent shared controls and disturbances included among the cases.The summary explicitly treats systems with shared states and notes that no shared states yield straightforward decoupling.
  • BRS decomposition: For unsafe-state targets, the minimal BRS can likewise be reconstructed from subsystem results, with avoiding unsafe states in either subsystem sufficient under the stated coupling.Theorem 2 formalizes this dual interpretation for states that will reach the unsafe target for all controls.
  • Proof strategy: The proofs relate full-system trajectories to projected subsystem trajectories and use back-projection to establish both reconstruction directions.The argument applies existential control quantifiers to subsystem reachability conditions.

B. Proof of Theorem 2

The section completes the unsafe-target reconstruction argument and illustrates the decomposition method on the Dubins Car. The numerical comparison yields indistinguishable BRSs while reducing computation to lower-dimensional problems and improving computational efficiency.

  • Proof of Theorem 2: Theorem 2’s proof replaces maximal-target BRSs with complementary minimal BRSs and applies the same projection argument to unsafe-state reconstruction.The proof uses complementary targets and corresponding back-projected subsystem sets.
  • Numerical example: The Dubins Car experiment computes unsafe BRSs at t = -0.5 from position targets near the origin and compares direct and decomposed formulations.The target is interpreted as an obstacle that the vehicle may collide with after duration |t|.
  • Computational benefits: Direct 3D computation becomes increasingly time-consuming as grid resolution rises, whereas 2D decomposed computation remains negligible in comparison.The comparison is reported using computation time against grid points per dimension on a log-log scale.
  • Numerical comparison: The direct and decomposed full-dimensional Dubins Car BRSs are indistinguishable when superimposed and viewed from multiple angles.The decomposed BRS is reconstructed by intersecting back-projections of the two subsystem BRSs.
  • Computational benefits: Lower-dimensional decomposition is significantly faster and can slightly improve HJ-PDE numerical accuracy because numerical dissipation grows with state dimension.The method computes subsystem BRSs in lower-dimensional subspaces before reconstruction.

V. SCSS WITH DECOUPLED CONTROL

This section treats self-contained subsystems with decoupled controls. Shared-state trajectories can then be treated as fixed inputs, yielding subsystem dynamics that support separate reachability computations.

  • Decoupled controls: When subsystem controls have no shared components, the common-state trajectory is independent of control and can be treated as fixed once the initial common state and time are given.This converts the remaining state partitions into self-contained controlled subsystems.
  • Decoupled controls: The resulting subsystem dynamics take the form f_i(z_i, z_c, u_i) = f_i(z_i, u_i; η_c(s; z_c, t)), with the common trajectory entering as a known parameter.Each subsystem retains its own control u_i while depending on the shared-state trajectory.
  • Special case: Fully decoupled systems with x1 = z1 and x2 = z2 are a special case, illustrated later using the 10D Near-Hover Quadrotor.The example is identified as a numerical demonstration of this control-decoupled setting.

B. Proof of Proposition 2

The section establishes how backward reachable sets and tubes relate under subsystem decomposition, including when tube reconstruction is direct or requires unions of reachable sets.

  • Control coupling: The BRS results for shared-control systems are weaker than those for systems whose subsystem controls have no shared components.State coupling does not prevent the theorems, but shared controls can produce inconsistent subsystem control choices.
  • BRT reconstruction: BRTs provide guarantees over a time horizon, unlike BRSs, which concern a particular time.For safety analysis, a BRT contains states leading to an unsafe state at some time within the horizon.
  • BRT reconstruction: When the target is a union of lifted subsystem targets, the full-dimensional BRT can be reconstructed from lower-dimensional BRTs without additional approximation errors.This case is covered by Proposition 3 and related results for self-contained subsystems.
  • BRT reconstruction: For an intersection of lifted subsystem targets, direct BRT reconstruction fails because tube computation loses the exact time at which trajectories enter a set.The general alternative is to compute subsystem BRSs and take their union to obtain the BRT.
  • BRT reconstruction: In the intersection-target case, both subsystem trajectories must occupy their corresponding target sets simultaneously, which may not occur at overlapping times.The union-of-BRS construction handles this timing mismatch.

C. Proof of Proposition 4

The proof shows that a BRT equals the union of BRSs over the time interval, under the stated nonemptiness condition for minimal BRSs.

  • Maximal BRT: The union of maximal BRSs over s ∈[t,0] is converted into a trajectory-existence statement over some time in [t,0].Time invariance shifts the trajectory arguments, and the existential time and control quantifiers can be exchanged.
  • Maximal BRT: This trajectory-existence statement is equivalent to membership in the maximal BRT by its definition.The proof identifies the union with the set of states that can reach the target at some time in the horizon.
  • Minimal BRT: For minimal BRSs, the union over time is contained in the minimal BRT.The proof uses the universal-control condition defining minimal reachability.
  • Minimal BRT: If every minimal BRS A(s) is nonempty throughout [t,0], the union of these BRSs equals the minimal BRT.The proof derives the reverse inclusion by selecting a control that avoids the target at every time when a state is outside A(t).
  • Scope condition: When some A(s) is empty, the equality between the union of minimal BRSs and the minimal BRT is unresolved and may fail or hold.The paper identifies finding a weaker sufficient condition as future work.

E. Numerical Results

Numerical experiments compare direct and decomposed reachability computations on the Dubins Car and demonstrate decomposition for the 6D Acrobatic Quadrotor.

  • Dubins Car: The Dubins Car experiment compares a full 3D BRS computation with reconstruction from lower-dimensional subsystem BRSs.The decomposed BRS is reconstructed using back-projections and intersection.
  • Acrobatic Quadrotor: For the Acrobatic Quadrotor, the 6D dynamics are decomposed into two 4D subsystems sharing φ and ω.The subsystem states are x1=(px,vx,φ,ω) and x2=(py,vy,φ,ω).
  • Acrobatic Quadrotor: The 6D BRS is reconstructed from the subsystem BRSs, while 3D positional and velocity slices visualize the time-varying sets and their BRT union.The BRT appears as the gray surface encompassing the BRSs in the velocity slices.

B. The 10D Near-Hover Quadrotor

The Near-Hover Quadrotor experiment applies decomposition to a 10D model, producing exact BRS and BRT slices while describing the disturbance setting used in the broader analysis.

  • System decomposition: The 10D Near-Hover Quadrotor is decomposed into 4D, 4D, and 2D subsystems.The subsystem states separate the x, y, and vertical dynamics into x1, x2, and x3.
  • System decomposition: The system controls include desired pitch and roll angles and vertical thrust, while disturbances represent wind along three axes.The model uses controls (Sx,Sy) and Tz, with disturbance components (dx,dy,dz).
  • Numerical results: The computed 10D BRT is the union of BRSs over s ∈[−1,0], and the figures show colored BRS slices with the BRT as a black surface.The slices are taken at specified fixed velocity, position, and angular coordinates.
  • Numerical results: Exact BRS and BRT slices showing angular behavior were not known to be obtainable with previous methods for this high-dimensional model.The paper attributes this to the need to analyze the full high-dimensional system model.
  • Disturbances: With disturbances, subsystem disturbances may share components, and results are stronger when they do not.The disturbance analysis uses non-anticipative strategies and defines disturbance-aware BRSs and BRTs.

A. Self-Contained Subsystems

With disturbances, decomposition preserves exact reachable-set results when subsystem disturbances have no shared components, while shared disturbances introduce conservative approximations with directional guarantees.

  • Shared disturbances: A state in the reconstructed BRS is guaranteed to be able to reach the target under the disturbance formulation.
  • Shared disturbances: A state outside the reconstructed BRS is guaranteed to be able to avoid the target for the complementary result.
  • No shared disturbances: When subsystem disturbances have no shared components, the quantifier expression can be distributed and the stronger BRS results still hold.
  • Decoupled control: For decoupled controls with shared disturbances, the reconstructed BRS remains a conservative approximation, and conservative BRS approximations can still be obtained.
  • Shared disturbances: Shared disturbances prevent distributing the disturbance-dependent control quantifiers, so reconstructed BRSs become conservative approximations.The reconstructed BRS remains useful because every state it contains is guaranteed to reach the target.
  • Reachable tubes: With overlapping subsystem disturbances, reconstructed BRTs become conservative approximations, while some disturbance-free reconstruction results carry over unchanged.
  • Reachable tubes: For coupled control and disturbance, the union of subsystem BRSs becomes an under-approximation of the BRT, retaining a guarantee of target reachability.

D. Dubins Car with Disturbances

The Dubins Car example decomposes a 3D disturbed system into lower-dimensional subsystems sharing the heading disturbance. Shared disturbances make the reconstructed BRT an over-approximation, whereas removing that shared component yields an exact match.

  • System setup: The disturbed Dubins Car uses state z = (px, py, θ), control u = ω, and disturbances d = (dx, dy, dθ), with θ overlapping between subsystems.The disturbance bounds are |dx| ≤ d̄x, |dy| ≤ d̄y, and |dθ| ≤ d̄θ; dθ is shared by both subsystem disturbances.
  • Shared disturbances: At t = −0.5, decomposition compares a 2D reconstruction against the directly computed 3D Dubins Car BRT.The example uses d̄x, d̄y = 1 and d̄θ = 5.
  • Shared disturbances: With shared disturbances, the decomposed BRT is an over-approximation of the true BRT.The over-approximation appears where the reconstructed black set is not flush against the directly computed red set.
  • No shared disturbances: With d̄θ = 0 and therefore no shared disturbance component, the directly computed 3D and decomposed 2D BRTs are the same.
  • Implications: The method reduces computation burden by working in lower-dimensional subspaces without sacrificing optimality in the presented scenarios.The paper reports orders-of-magnitude faster computations and slightly conservative approximations under some disturbances.
  • Future work: The authors identify extensions to additional full-dimensional representations, system-dynamics families, learning-based automation, and hardware experiments.
Loading 1611.00122v3…