pith. sign in

arxiv: 2604.05108 · v1 · submitted 2026-04-06 · 📡 eess.SY · cs.RO· cs.SY

Differentiable Invariant Sets for Hybrid Limit Cycles with Application to Legged Robots

Varun Madabushi , Akash Harapanahalli , Samuel Coogan , Maegan Tucker This is my paper

Pith reviewed 2026-05-10 18:48 UTC · model grok-4.3

classification 📡 eess.SY cs.ROcs.SY
keywords hybrid systemsinvariant setsreachable setslimit cycleslegged robotsparametric embeddingsbipedal robotsformal verification
0
0 comments X

The pith

If the overapproximated reachable set after one hybrid step is a strict subset of the initial set, a forward invariant set for the hybrid periodic orbit is formally verified.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

This paper extends parametric embedding techniques from continuous systems to hybrid systems to compute forward-invariant sets around limit cycles. The approach involves overapproximating the reachable set for the continuous flow, cataloging intersections with the guard, and applying the reset map. For a bipedal robot model, if the final overapproximated set is strictly inside the initial one, the invariant set is verified. This verification is performed numerically and used to optimize a tracking controller that enlarges the invariant set.

Core claim

The central claim is that for hybrid periodic orbits, a three-step overapproximation of reachable sets via parametric embeddings verifies a forward invariant set containing the orbit whenever the approximated set after one full step is strictly contained in the starting set.

What carries the argument

Parametric embeddings for overapproximating reachable sets in hybrid systems, handling continuous flows, guard intersections, and reset maps.

If this is right

  • If the condition holds, the invariant set provides a formal guarantee of robustness for the periodic behavior.
  • The bi-level optimization can tune controller parameters to increase the size of this verified set.
  • The numerical method using differentiable computation applies directly to simplified models of contact-rich legged locomotion.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • This could support designing controllers with explicit robustness certificates for legged robots in uncertain environments.
  • The differentiability of the embeddings opens possibilities for gradient-based search over larger classes of controllers or gaits.
  • Similar verification might apply to other hybrid systems exhibiting periodic orbits beyond robotics.

Load-bearing premise

The overapproximations from the parametric embeddings are tight enough to capture the true reachable sets without excessive added volume or undetected numerical errors.

What would settle it

Compute the overapproximated reachable set for the bipedal model starting from a candidate initial set; if it is not strictly smaller after one step, or if trajectories from within the set leave the verified invariant set, the claim does not hold for that instance.

Figures

Figures reproduced from arXiv: 2604.05108 by Akash Harapanahalli, Maegan Tucker, Samuel Coogan, Varun Madabushi.

Figure 1
Figure 1. Figure 1: A visualization of the conditions supposed in Theorem 1. While [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: The slicing and bounding procedure used in Lemma 1 and Theorem [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Simplified Bipedal Walker illustrated for the (a) continuous domain, [PITH_FULL_IMAGE:figures/full_fig_p006_3.png] view at source ↗
Figure 5
Figure 5. Figure 5: Slices of the computed Hybrid Invariant Tube with no tracking [PITH_FULL_IMAGE:figures/full_fig_p007_5.png] view at source ↗
read the original abstract

For hybrid systems exhibiting periodic behavior, analyzing the invariant set containing the limit cycle is a natural way to study the robustness of the closed-loop system. However, computing these sets can be computationally expensive, especially when applied to contact-rich cyber-physical systems such as legged robots. In this work, we extend existing methods for overapproximating reachable sets of continuous systems using parametric embeddings to compute a forward-invariant set around the nominal trajectory of a simplified model of a bipedal robot. Our three-step approach (i) computes an overapproximating reachable set around the nominal continuous flow, (ii) catalogs intersections with the guard surface, and (iii) passes these intersections through the reset map. If the overapproximated reachable set after one step is a strict subset of the initial set, we formally verify a forward invariant set for this hybrid periodic orbit. We verify this condition on the bipedal walker model numerically using immrax, a JAX-based library for parametric reachable set computation, and use it within a bi-level optimization framework to design a tracking controller that maximizes the size of the invariant set.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The manuscript extends parametric embedding techniques for overapproximating reachable sets of continuous systems to hybrid dynamics. It proposes a three-step procedure—(i) overapproximate the continuous flow around a nominal trajectory, (ii) catalog intersections with the guard surface, (iii) apply the reset map—to compute a forward-invariant set around a hybrid limit cycle. If the one-step overapproximated image is a strict subset of the initial set, invariance is formally verified. The method is implemented numerically via the immrax JAX library on a simplified bipedal walker model and embedded in a bi-level optimization to synthesize a tracking controller that maximizes the size of the verified invariant set.

Significance. If the overapproximations are valid and sufficiently tight, the approach would offer a practical route to certifying robustness of periodic orbits in contact-rich hybrid systems such as legged robots, where exact invariant-set computation is intractable. The differentiable, JAX-native implementation is a concrete strength that directly supports the bi-level controller synthesis loop.

major comments (2)
  1. [§3] §3 (Hybrid reachable-set procedure): the claim that the post-reset image being a strict subset of the initial set formally verifies forward invariance rests on the three-step overapproximation being a true superset of all hybrid trajectories. Step (ii) catalogs guard intersections but does not specify how the continuous dependence of crossing times on the embedding parameters is conservatively overapproximated; a fixed-time or non-validated event detection can exclude reachable crossing states, so the reset-map image need not contain the true hybrid successor set and the subset test no longer implies invariance.
  2. [Numerical results] Numerical results section: the abstract asserts that the condition is verified numerically on the biped model, yet no concrete reachable-set volumes, Hausdorff distances to the nominal orbit, tightness ratios, or comparison against a ground-truth simulator are reported. Without these metrics it is impossible to judge whether the immrax implementation produces usable (non-vacuous) overapproximations or whether the bi-level optimization actually enlarges a meaningful invariant set.
minor comments (2)
  1. [Preliminaries] The notation for the parametric embedding family and the hybrid reachable-set operator should be introduced with explicit set-valued definitions before the three-step algorithm is stated.
  2. [Figures] Figure captions should state whether the plotted sets are the initial tube, the one-step image, or both, and should indicate the embedding dimension used.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the thoughtful and detailed review. The comments identify important points for clarification and strengthening of the presentation. We address each major comment below and outline the revisions we will make.

read point-by-point responses

  1. Referee: [§3] §3 (Hybrid reachable-set procedure): the claim that the post-reset image being a strict subset of the initial set formally verifies forward invariance rests on the three-step overapproximation being a true superset of all hybrid trajectories. Step (ii) catalogs guard intersections but does not specify how the continuous dependence of crossing times on the embedding parameters is conservatively overapproximated; a fixed-time or non-validated event detection can exclude reachable crossing states, so the reset-map image need not contain the true hybrid successor set and the subset test no longer implies invariance.

    Authors: We agree that the manuscript must explicitly establish that the three-step procedure produces a true superset of the hybrid successor set. In the current draft the description of step (ii) is concise and does not detail the validated event-detection mechanism. The immrax implementation propagates the parametric embedding with interval arithmetic and uses a validated integrator that encloses all possible crossing times; the guard intersections are therefore computed as an over-approximating set rather than at fixed times. Nevertheless, this technical detail is not stated clearly enough in §3. We will expand the section with a short paragraph (and a supporting lemma) that shows how the continuous dependence of crossing times is enclosed by the parametric reachable-set computation, thereby guaranteeing that the post-reset image contains every possible hybrid successor. With this addition the subset test will correctly imply forward invariance. revision: yes

  2. Referee: [Numerical results] Numerical results section: the abstract asserts that the condition is verified numerically on the biped model, yet no concrete reachable-set volumes, Hausdorff distances to the nominal orbit, tightness ratios, or comparison against a ground-truth simulator are reported. Without these metrics it is impossible to judge whether the immrax implementation produces usable (non-vacuous) overapproximations or whether the bi-level optimization actually enlarges a meaningful invariant set.

    Authors: We concur that quantitative metrics are essential for assessing the practical value of the over-approximations. The current numerical section reports only that the invariance condition holds and that the optimized controller yields a larger set; it does not supply volumes, Hausdorff distances, tightness ratios, or simulator comparisons. In the revised manuscript we will add a dedicated subsection that reports: (i) the volume of the initial and one-step over-approximated sets, (ii) the Hausdorff distance between the over-approximated set and the nominal orbit, (iii) a tightness ratio obtained by comparing the over-approximation against a high-fidelity Monte-Carlo simulation of the biped, and (iv) the improvement in these quantities achieved by the bi-level controller optimization. These additions will allow readers to judge both the conservatism of the reachable-set computation and the effectiveness of the synthesis procedure. revision: yes

Circularity Check

0 steps flagged

No significant circularity in reachable-set overapproximation or invariance check

full rationale

The paper's derivation proceeds by (i) parametric embedding to overapproximate continuous flows, (ii) cataloging guard intersections, and (iii) applying the reset map, followed by a direct set-inclusion test against the initial set. This inclusion test is performed via calls to an external library (immrax) on the given model dynamics and does not reduce to any fitted parameter, self-referential definition, or load-bearing self-citation. The central claim therefore remains independent of its own outputs and is self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claim rests on the validity of extending continuous-system overapproximations to hybrid jumps and on the existence of a periodic orbit in the chosen biped model; no new physical entities are introduced.

axioms (2)
  • domain assumption The simplified bipedal walker model possesses a hybrid periodic orbit.
    Required to apply the invariance test to the legged-robot example.
  • domain assumption Parametric embeddings yield valid overapproximations of reachable sets for the continuous dynamics.
    Inherited from prior continuous-system methods and extended without additional proof in the abstract.

pith-pipeline@v0.9.0 · 5512 in / 1315 out tokens · 61070 ms · 2026-05-10T18:48:15.729926+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

26 extracted references · 26 canonical work pages

  1. [1]

    Hybrid dynamical systems,

    R. Goebel, R. G. Sanfelice, and A. R. Teel, “Hybrid dynamical systems,”IEEE control systems magazine, pp. 28–93, 2009

    work page 2009

  2. [2]

    Sastry,Nonlinear systems: analysis, stability, and control, vol

    S. Sastry,Nonlinear systems: analysis, stability, and control, vol. 10. Springer Science & Business Media, 2013

    work page 2013

  3. [3]

    Hybrid zero dynamics of planar biped walkers,

    E. R. Westervelt, J. W. Grizzle, and D. E. Koditschek, “Hybrid zero dynamics of planar biped walkers,”IEEE transactions on automatic control, vol. 48, no. 1, pp. 42–56, 2003

    work page 2003

  4. [4]

    Planning and control for dynamic, nonprehensile, and hybrid manipulation tasks,

    J. Z. Woodruff and K. M. Lynch, “Planning and control for dynamic, nonprehensile, and hybrid manipulation tasks,” inInternational Con- ference on Robotics and Automation (ICRA), IEEE, 2017

    work page 2017

  5. [5]

    Hybrid control for a class of underactuated mechanical systems,

    R. Fierro, F. L. Lewis, and A. Lowe, “Hybrid control for a class of underactuated mechanical systems,”IEEE Transactions on Systems, Man, and Cybernetics-Part A: Systems and Humans, 2002

    work page 2002

  6. [6]

    H. K. Khalil and J. W. Grizzle,Nonlinear systems, vol. 3. Prentice hall Upper Saddle River, NJ, 2002

    work page 2002

  7. [7]

    Local stability analysis using simulations and sum-of-squares programming,

    U. Topcu, A. Packard, and P. Seiler, “Local stability analysis using simulations and sum-of-squares programming,”Automatica, vol. 44, no. 10, pp. 2669–2675, 2008

    work page 2008

  8. [8]

    Transverse dynamics and regions of stability for nonlinear hybrid limit cycles,

    I. R. Manchester, “Transverse dynamics and regions of stability for nonlinear hybrid limit cycles,”IFAC Proceedings Volumes, vol. 44, no. 1, pp. 6285–6290, 2011

    work page 2011

  9. [9]

    Chesi,Domain of attraction: analysis and control via SOS pro- gramming, vol

    G. Chesi,Domain of attraction: analysis and control via SOS pro- gramming, vol. 415. Springer Science & Business Media, 2011

    work page 2011

  10. [10]

    A time-dependent hamilton-jacobi formulation of reachable sets for continuous dynamic games,

    I. M. Mitchell, A. M. Bayen, and C. J. Tomlin, “A time-dependent hamilton-jacobi formulation of reachable sets for continuous dynamic games,”IEEE Transactions on automatic control, 2005

    work page 2005

  11. [11]

    Regions of attraction for hybrid limit cycles of walking robots,

    I. R. Manchester, M. M. Tobenkin, M. Levashov, and R. Tedrake, “Regions of attraction for hybrid limit cycles of walking robots,”IFAC Proceedings Volumes, vol. 44, no. 1, pp. 5801–5806, 2011

    work page 2011

  12. [12]

    Computation of regions of attraction for hybrid limit cycles using reachability: An application to walking robots,

    J. J. Choi, A. Agrawal, K. Sreenath, C. J. Tomlin, and S. Bansal, “Computation of regions of attraction for hybrid limit cycles using reachability: An application to walking robots,”IEEE Robotics and Automation Letters, vol. 7, no. 2, pp. 4504–4511, 2022

    work page 2022

  13. [13]

    Set propagation techniques for reachability analysis,

    M. Althoff, G. Frehse, and A. Girard, “Set propagation techniques for reachability analysis,”Annual Review of Control, Robotics, and Autonomous Systems, vol. 4, no. 1, pp. 369–395, 2021

    work page 2021

  14. [14]

    An Introduction to CORA 2015,

    M. Althoff, “An Introduction to CORA 2015,” inProc. of the 1st and 2nd Workshop on Applied Verification for Continuous and Hybrid Systems, pp. 120–151, EasyChair, Dec. 2015

    work page 2015

  15. [15]

    JuliaReach: a toolbox for set-based reachability,

    S. Bogomolov, M. Forets, G. Frehse, K. Potomkin, and C. Schilling, “JuliaReach: a toolbox for set-based reachability,” inProceedings of the 22nd ACM International Conference on Hybrid Systems: Compu- tation and Control, pp. 39–44, 2019

    work page 2019

  16. [16]

    Efficient interaction- aware interval analysis of neural network feedback loops,

    S. Jafarpour, A. Harapanahalli, and S. Coogan, “Efficient interaction- aware interval analysis of neural network feedback loops,”IEEE Transactions on Automatic Control, 2024

    work page 2024

  17. [17]

    immrax: A paral- lelizable and differentiable toolbox for interval analysis and mixed monotone reachability in jax,

    A. Harapanahalli, S. Jafarpour, and S. Coogan, “immrax: A paral- lelizable and differentiable toolbox for interval analysis and mixed monotone reachability in jax,”IFAC-PapersOnLine, 2024

    work page 2024

  18. [18]

    Jaulin, M

    L. Jaulin, M. Kieffer, O. Didrit, and E. Walter,Applied interval analysis. Springer, 1st edition. ed., 2001

    work page 2001

  19. [19]

    JAX: composable transformations of Python+NumPy programs,

    J. Bradbury, R. Frostig, P. Hawkins, M. J. Johnson, C. Leary, D. Maclaurin, G. Necula, A. Paszke, J. VanderPlas, S. Wanderman- Milne, and Q. Zhang, “JAX: composable transformations of Python+NumPy programs,” 2018

    work page 2018

  20. [20]

    Algorithmic foundations of realizing multi-contact locomotion on the humanoid robot durus,

    J. P. Reher, A. Hereid, S. Kolathaya, C. M. Hubicki, and A. D. Ames, “Algorithmic foundations of realizing multi-contact locomotion on the humanoid robot durus,” inAlgorithmic Foundations of Robotics XII: Proceedings of the Twelfth Workshop on the Algorithmic Foundations of Robotics, pp. 400–415, Springer, 2020

    work page 2020

  21. [21]

    A restricted poincar ´e map for deter- mining exponentially stable periodic orbits in systems with impulse effects: Application to bipedal robots,

    B. Morris and J. W. Grizzle, “A restricted poincar ´e map for deter- mining exponentially stable periodic orbits in systems with impulse effects: Application to bipedal robots,” inProceedings of the 44th IEEE Conference on Decision and Control, 2005

    work page 2005

  22. [22]

    A linear differential inclusion for contraction analysis to known trajectories,

    A. Harapanahalli and S. Coogan, “A linear differential inclusion for contraction analysis to known trajectories,”IEEE Transactions on Automatic Control, pp. 1–8, 2025

    work page 2025

  23. [23]

    Efficient norm-based reachable sets via iterative dynamic programming,

    A. Harapanahalli and S. Coogan, “Efficient norm-based reachable sets via iterative dynamic programming,”arXiv preprint arXiv:2509.23367, 2025

    work page arXiv 2025

  24. [24]

    Bullo,Contraction theory for dynamical systems

    F. Bullo,Contraction theory for dynamical systems. 2022

    work page 2022

  25. [25]

    Kidger,On Neural Differential Equations

    P. Kidger,On Neural Differential Equations. PhD thesis, University of Oxford, 2021

    work page 2021

  26. [26]

    cyipopt,

    J. K. Moore, “cyipopt,” 08 2025

    work page 2025