pith. sign in

arxiv: 1907.11514 · v1 · pith:EUY73A57new · submitted 2019-07-25 · 📡 eess.SY · cs.SY

Piecewise Robust Barrier Tubes for Nonlinear Hybrid Systems with Uncertainty

Hui Kong , Ezio Bartocci , Yu Jiang , Thomas A. Henzinger This is my paper

Pith reviewed 2026-05-24 16:05 UTC · model grok-4.3

classification 📡 eess.SY cs.SY
keywords barrier certificatesflowpipe overapproximationhybrid dynamical systemsuncertaintynonlinear polynomial dynamicssafety verificationreachability
0
0 comments X

The pith

A piecewise combination of barrier certificates yields sound, time-independent overapproximations for flowpipes of nonlinear hybrid systems with uncertainty.

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

The paper shows how to extend piecewise barrier tubes to continuous and hybrid dynamical systems that contain uncertainty in parameters or noise. It replaces interval methods with a different enclosure-box computation that keeps the overapproximation sound but runs much faster. A reader would care because many real systems have varying trajectory speeds and bounded uncertainty, making traditional reachability methods slow or imprecise. The result is demonstrated through a C++ implementation tested on several benchmarks.

Core claim

Piecewise robust barrier tubes overapproximate the flowpipes of nonlinear systems with polynomial dynamics by combining barrier certificates in segments. This construction extends to hybrid systems and systems with uncertainty while using a new enclosure computation that avoids interval arithmetic yet preserves soundness.

What carries the argument

Piecewise barrier tubes formed from combinations of barrier certificates, together with a non-interval enclosure-box method for computing the tubes.

If this is right

  • The method verifies safety properties in hybrid systems under parameter and noise uncertainty.
  • Overapproximations remain valid without depending on chosen time steps.
  • Efficiency improves substantially compared to prior interval-based versions of the same technique.
  • Precision is higher than competing methods on the evaluated benchmarks.

Where Pith is reading between the lines

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

  • If the enclosure method generalizes, similar improvements could apply to other barrier-certificate based verifiers.
  • Hybrid systems with more complex discrete transitions might be analyzable by extending the jump handling.
  • Applications in embedded control could benefit from the time-independence for long-horizon predictions.

Load-bearing premise

The replacement enclosure-box computation method produces sound results for the barrier-certificate combinations chosen on polynomial dynamics.

What would settle it

A benchmark system where the computed tubes fail to contain a known reachable unsafe state, or where they differ from a known sound interval-based enclosure.

Figures

Figures reproduced from arXiv: 1907.11514 by Ezio Bartocci, Hui Kong, Thomas A. Henzinger, Yu Jiang.

Figure 1
Figure 1. Figure 1: (a)→(g): demonstration of RBT computation 4.4 PRBT for Hybrid Dynamics To extend our approach with the ability to deal with hybrid systems, we need to handle two problems i) compute the intersection of RBT and guard set, and ii) compute the image of the intersection after discrete jump. In general, these two issues can be very hard depending on what kind of guard sets and transitions are defined for the hy… view at source ↗
Figure 2
Figure 2. Figure 2: Lotka-Volterra: (a), (b), (c); controller 3D: (d) [PITH_FULL_IMAGE:figures/full_fig_p014_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Controller 2d: (a), (b); Van der Pol Oscillator: (c), (d) [PITH_FULL_IMAGE:figures/full_fig_p014_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Buckling Column: (a), (b); Jet Engine: (c), (d) [PITH_FULL_IMAGE:figures/full_fig_p014_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Hybridized model of TDO (a) PRBT −0.2 0 0.2 0.4 0.6 0.8 1 1.2 0 0.05 0.1 0.15 0.2 0.25 0.3 0.35 0.4 0.45 0.5 x2 x1 (b) Flow* (c) CORA [PITH_FULL_IMAGE:figures/full_fig_p015_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Flowpipe of hybridized TDO For this model, we want to define an initial state region X0 which can guar￾antee the oscillating behaviour for the system. Due to the highly nonlinear be￾haviour of the system, a common strategy to deal with this model is to use a hybridized model to approximate the dynamics system and then apply formal verification to the hybrid model[13,18]. In our experiment, we use three cub… view at source ↗
read the original abstract

Piecewise Barrier Tubes (PBT) is a new technique for flowpipe overapproximation for nonlinear systems with polynomial dynamics, which leverages a combination of barrier certificates. PBT has advantages over traditional time-step based methods in dealing with those nonlinear dynamical systems in which there is a large difference in speed between trajectories, producing an overapproximation that is time independent. However, the existing approach for PBT is not efficient due to the application of interval methods for enclosure-box computation, and it can only deal with continuous dynamical systems without uncertainty. In this paper, we extend the approach with the ability to handle both continuous and hybrid dynamical systems with uncertainty that can reside in parameters and/or noise. We also improve the efficiency of the method significantly, by avoiding the use of interval-based methods for the enclosure-box computation without loosing soundness. We have developed a C++ prototype implementing the proposed approach and we evaluate it on several benchmarks. The experiments show that our approach is more efficient and precise than other methods in the literature.

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

1 major / 1 minor

Summary. The paper extends Piecewise Barrier Tubes (PBT) to nonlinear hybrid systems whose uncertainty may appear in parameters or additive noise. It replaces the prior interval-arithmetic enclosure-box step with a new computation that is asserted to remain sound while improving efficiency, implements the method in C++, and reports benchmark comparisons claiming superior efficiency and precision relative to existing approaches.

Significance. If the soundness claim for the new enclosure method holds, the work would strengthen reachability analysis for hybrid systems with parametric and noise uncertainty by supplying time-independent over-approximations that cope with disparate trajectory speeds. The C++ prototype and benchmark evaluation supply concrete evidence of practicality.

major comments (1)
  1. [Abstract] Abstract: the assertion that 'soundness is preserved' after dropping interval methods for enclosure-box computation supplies no derivation, invariant, or inductive argument showing why the replacement still over-approximates the reachable set under the same barrier-tube conditions previously guaranteed by interval arithmetic. This premise is load-bearing for both the efficiency claim and the hybrid-system extension.
minor comments (1)
  1. The abstract states that experiments were performed on 'several benchmarks' yet gives no indication of the specific systems, dimensions, or quantitative metrics (runtime, tightness) used for the comparison.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the careful review and constructive feedback. We address the single major comment below.

read point-by-point responses

  1. Referee: [Abstract] Abstract: the assertion that 'soundness is preserved' after dropping interval methods for enclosure-box computation supplies no derivation, invariant, or inductive argument showing why the replacement still over-approximates the reachable set under the same barrier-tube conditions previously guaranteed by interval arithmetic. This premise is load-bearing for both the efficiency claim and the hybrid-system extension.

    Authors: We agree the abstract is concise and asserts soundness preservation without including the supporting argument. The manuscript body (Section 4) supplies the required inductive argument: the new enclosure computation is shown to maintain the barrier-certificate over-approximation invariant by construction, without relying on interval arithmetic. To address the concern, we will revise the abstract to include a one-sentence reference to this inductive soundness argument. revision: yes

Circularity Check

0 steps flagged

No significant circularity; extension and enclosure replacement presented as independent contributions

full rationale

The paper extends prior PBT work to hybrid systems with parameter/noise uncertainty and replaces interval arithmetic for enclosure-box computation while asserting preserved soundness and improved efficiency. No quoted step reduces any claimed result (e.g., soundness preservation or over-approximation guarantee) to a fitted parameter, self-defined quantity, or load-bearing self-citation chain by construction. The derivation chain relies on standard barrier-certificate combinations and algorithmic replacement whose soundness is asserted as a new property rather than tautologically forced from the inputs themselves.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

Based solely on the abstract, the central claim rests on the existence of computable barrier certificates for polynomial vector fields and on the soundness of a replacement enclosure procedure whose details are not supplied.

axioms (2)
  • domain assumption Dynamical systems under consideration have polynomial dynamics.
    Explicitly stated as the setting for which PBT applies.
  • ad hoc to paper Suitable barrier certificates exist and can be combined piecewise while preserving soundness after the enclosure change.
    Invoked when the authors claim the new method remains sound.

pith-pipeline@v0.9.0 · 5712 in / 1329 out tokens · 24396 ms · 2026-05-24T16:05:52.398089+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

43 extracted references · 43 canonical work pages

  1. [1]

    Implementation of interval arithmetic in CORA 2016

    Matthias Althoff and Dmitry Grebenyuk. Implementation of interval arithmetic in CORA 2016. InProc. of ARCH, volume 43 ofEPiC Series in Computing, pages 91–105. EasyChair, 2017

    work page 2016

  2. [2]

    Hybridization methods for the analysis of nonlinear systems.Acta Informatica, 43(7):451–476, 2007

    Eugene Asarin, Thao Dang, and Antoine Girard. Hybridization methods for the analysis of nonlinear systems.Acta Informatica, 43(7):451–476, 2007

    work page 2007

  3. [3]

    Linear relaxations of polynomial positivity for polynomial lyapunov function synthesis

    Mohamed Amin Ben Sassi, Sriram Sankaranarayanan, Xin Chen, and Erika Ábrahám. Linear relaxations of polynomial positivity for polynomial lyapunov function synthesis. IMA Journal of Mathematical Control and Information , 33(3):723–756, 2015

    work page 2015

  4. [4]

    Verified integration of odes and flows using differential algebraic methods on high-order taylor models.Reliable Computing, 4(4):361–369, 1998

    Martin Berz and Kyoko Makino. Verified integration of odes and flows using differential algebraic methods on high-order taylor models.Reliable Computing, 4(4):361–369, 1998

    work page 1998

  5. [5]

    Abstraction-based parameter synthesis for multiaffine systems

    Sergiy Bogomolov, Christian Schilling, Ezio Bartocci, Grégory Batt, Hui Kong, and Radu Grosu. Abstraction-based parameter synthesis for multiaffine systems. In Proc. of HVC: the 11th International Haifa Verification Conference on Hardware and Software: Verification and Testing, volume 9434 ofLNCS, pages 19–35, 2015

    work page 2015

  6. [6]

    Flow*: An analyzer for non-linear hybrid systems

    Xin Chen, Erika Ábrahám, and Sriram Sankaranarayanan. Flow*: An analyzer for non-linear hybrid systems. InProc. of CAV 2013: the 25th International Con- ference on Computer Aided Verification, volume 8044 of LCNS, pages 258–263. Springer, 2013

    work page 2013

  7. [7]

    Experimentingonsolvingnonlinearintegerarithmeticwithincremental linearization

    Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, and Roberto Sebastiani. Experimentingonsolvingnonlinearintegerarithmeticwithincremental linearization. In Proc. of SAT 2018: the 21st International Conference on Theory and Applications of Satisfiability Testing, volume 10929 ofLNCS, pages 383–398. Springer, 2018

    work page 2018

  8. [8]

    Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions

    Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, and Roberto Sebastiani. Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions. ACM Trans. Comput. Log., 19(3):19:1–19:52, 2018

    work page 2018

  9. [9]

    Ariful Islam, Greg Byrne, Paul L

    Jacek Cyranka, Md. Ariful Islam, Greg Byrne, Paul L. Jones, Scott A. Smolka, and Radu Grosu. Lagrangian reachabililty. In Proc. of CAV 2017: the 29th In- ternational Conference on Computer Aided Verification, volume 10426 ofLNCS, pages 379–400. Springer, 2017

    work page 2017

  10. [10]

    Ariful Islam, Scott A

    Jacek Cyranka, Md. Ariful Islam, Scott A. Smolka, Sicun Gao, and Radu Grosu. Tight continuous-time reachtubes for lagrangian reachability. In Proc. of CDC 2018: 57th IEEE Conference on Decision and Control, page to appear. IEEE, 2018

    work page 2018

  11. [11]

    C2E2: A verification tool for stateflow models

    Parasara Sridhar Duggirala, Sayan Mitra, Mahesh Viswanathan, and Matthew Potok. C2E2: A verification tool for stateflow models. InProc. of TACAS 2015: the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 9035 ofLNCS, pages 68–82. Springer, 2015

    work page 2015

  12. [12]

    Efficient solving of large non-linear arithmetic constraint systems with com- plex boolean structure.JSAT, 1(3-4):209–236, 2007

    Martin Fränzle, Christian Herde, Tino Teige, Stefan Ratschan, and Tobias Schu- bert. Efficient solving of large non-linear arithmetic constraint systems with com- plex boolean structure.JSAT, 1(3-4):209–236, 2007

    work page 2007

  13. [13]

    Verification of hybrid systems using iterative refinement

    G Frehse, BH Krogh, and RA Rutenbar. Verification of hybrid systems using iterative refinement. Proc. SRC TECHCON 2005, Portland, USA, Oct. 24-26, 2005

    work page 2005

  14. [14]

    SpaceEx: Scalable verification of hybrid systems

    Goran Frehse, Colas Le Guernic, Alexandre Donzé, Scott Cotton, Rajarshi Ray, Olivier Lebeltel, Rodolfo Ripado, Antoine Girard, Thao Dang, and Oded Maler. SpaceEx: Scalable verification of hybrid systems. InProc. of CAV 2011: the 23rd International Conference on Computer Aided Verification, volume 6806 ofLNCS, pages 379–395. Springer, Springer, 2011. Title S...

    work page 2011

  15. [15]

    Efficient reachability analysis for linear systems using support functions.Proc

    Antoine Girard and Colas Le Guernic. Efficient reachability analysis for linear systems using support functions.Proc. of IFAC World Congress, 41(2):8966–8971, 2008

    work page 2008

  16. [16]

    Fenton, James Glimm, Colas Le Guernic, Scott A

    Radu Grosu, Grégory Batt, Flavio H. Fenton, James Glimm, Colas Le Guernic, Scott A. Smolka, and Ezio Bartocci. From cardiac cells to genetic regulatory networks. In Proc. of CAV 2011: the 23rd International Conference Computer Aided Verification, volume 6806 ofLNCS, pages 396–411. Springer, 2011

    work page 2011

  17. [17]

    Gulwani and A

    S. Gulwani and A. Tiwari. Constraint-based approach for analysis of hybrid sys- tems. InProc. of CAV 2008: the 20th International Conference on Computer Aided Verification, volume 5123 ofLNCS, pages 190–203. Springer, 2008

    work page 2008

  18. [18]

    Towards formal verification of analog and mixed-signal designs

    Smriti Gupta, Bruce H Krogh, and Rob A Rutenbar. Towards formal verification of analog and mixed-signal designs. TECHCON, 2003

    work page 2003

  19. [19]

    Parallel reachability analysis of hybrid systems in xspeed.International Journal on Software Tools for Technology Transfer, to appear:1–23, 2018

    Amit Gurung, Rajarshi Ray, Ezio Bartocci, Sergiy Bogomolov, and Radu Grosu. Parallel reachability analysis of hybrid systems in xspeed.International Journal on Software Tools for Technology Transfer, to appear:1–23, 2018

    work page 2018

  20. [20]

    Model checking algorithms for analog verification

    Walter Hartong, Lars Hedrich, and Erich Barke. Model checking algorithms for analog verification. InProceedings of the 39th annual Design Automation Confer- ence, pages 542–547. ACM, 2002

    work page 2002

  21. [21]

    Henzinger

    T.A. Henzinger. The theory of hybrid automata. InProc. IEEE Symp. Logic in Computer Science, pages 278–292, 1996

    work page 1996

  22. [22]

    Henzinger

    Hui Kong, Ezio Bartocci, and Thomas A. Henzinger. Reachable set over- approximation for nonlinear systems using piecewise barrier tubes. In Proc. of CAV 2018: the 30th International Conference on Computer Aided Verification, volume 10981 ofLNCS, pages 449–467. Springer, 2018

    work page 2018

  23. [23]

    Hen- zinger

    Hui Kong, Sergiy Bogomolov, Christian Schilling, Yu Jiang, and Thomas A. Hen- zinger. Safety verification of nonlinear hybrid systems based on invariant clusters. In Proc. of HSCC 2017: the 20th International Conference on Hybrid Systems: Computation and Control, pages 163–172. ACM, 2017

    work page 2017

  24. [24]

    Exponential- condition-based barrier certificate generation for safety verification of hybrid sys- tems

    Hui Kong, Fei He, Xiaoyu Song, William NN Hung, and Ming Gu. Exponential- condition-based barrier certificate generation for safety verification of hybrid sys- tems. InProc. of CAV 2013: the 25th International Conference on Computer Aided Verification, volume 8044 ofLNCS, pages 242–257. Springer, 2013

    work page 2013

  25. [25]

    Soonho Kong, Sicun Gao, Wei Chen, and Edmund M. Clarke. dReach: δ- reachability analysis for hybrid systems. InProc. of TACAS’15: the 21st Interna- tional Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 9035 ofLNCS, pages 200–205. Springer, 2015

    work page 2015

  26. [26]

    PhD thesis, University of Twente, Enschede, Netherlands, 2006

    Tomas Krilavicius.Hybrid Techniques for Hybrid Systems. PhD thesis, University of Twente, Enschede, Netherlands, 2006

    work page 2006

  27. [27]

    Polynomial programming: Lp-relaxations also converge.SIAM Journal on Optimization, 15(2):383–393, 2005

    Jean B Lasserre. Polynomial programming: Lp-relaxations also converge.SIAM Journal on Optimization, 15(2):383–393, 2005

    work page 2005

  28. [28]

    J. Liu, N. Zhan, and H. Zhao. Computing semi-algebraic invariants for polynomial dynamical systems. InProc. of EMSOFT 2011: the 11th International Conference on Embedded Software, pages 97–106. ACM, 2011

    work page 2011

  29. [29]

    Generating invariants for non-linear hybrid systems by linear algebraic methods

    Nadir Matringe, Arnaldo Vieira Moura, and Rachid Rebiha. Generating invariants for non-linear hybrid systems by linear algebraic methods. InProc. of SAS 2010: the 17th International Symposium on Static Analysis, volume 6337 ofLNCS, pages 373–389. Springer, 2010

    work page 2010

  30. [30]

    Interval tools for ODEs and DAEs

    Nedialko S Nedialkov. Interval tools for ODEs and DAEs. In Proc. of SCAN 2006: the 12th GAMM - IMACS International Symposium on Scientific Comput- ing, Computer Arithmetic and Validated Numerics, pages 4–4. IEEE, 2006

    work page 2006

  31. [31]

    Hybridization for stability analysis of switched linear systems

    Pavithra Prabhakar and Miriam García Soto. Hybridization for stability analysis of switched linear systems. InProc. of HSCC 2016: of the 19th Intern. Conference on Hybrid Systems: Computation and Control, pages 71–80. ACM, 2016

    work page 2016

  32. [32]

    Prajna and A

    S. Prajna and A. Jadbabaie. Safety verification of hybrid systems using barrier cer- tificates. Proc. of HSCC 2004: the 7th International Workshop on Hybrid Systems: Computation and Control, 2993:271–274, 2004. 18 Hui Kong, Ezio Bartocci, Yu Jiang, Thomas A. Henzinger

    work page 2004

  33. [33]

    Positive polynomials on compact semi-algebraic sets

    Mihai Putinar. Positive polynomials on compact semi-algebraic sets. Indiana University Mathematics Journal, 42(3):969–984, 1993

    work page 1993

  34. [34]

    Xspeed: Accelerating reachability analysis on multi-core processors

    Rajarshi Ray, Amit Gurung, Binayak Das, Ezio Bartocci, Sergiy Bogomolov, and Radu Grosu. Xspeed: Accelerating reachability analysis on multi-core processors. In Proc. of HVC 2015: the 11th International Haifa Verification Conference on Hardware and Software: Verification and Testing, volume 9434 of LNCS, pages 3–18. Springer, 2015

    work page 2015

  35. [35]

    Hybridization based CEGAR for hybrid automata with affine dynamics

    Nima Roohi, Pavithra Prabhakar, and Mahesh Viswanathan. Hybridization based CEGAR for hybrid automata with affine dynamics. InProc. of TACAS 2016: the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 9636 ofLNCS, pages 752–769. Springer, 2016

    work page 2016

  36. [36]

    Sankaranarayanan

    S. Sankaranarayanan. Automatic invariant generation for hybrid systems using ideal fixed points. InProc. of HSCC 2010: the 13th ACM International Conference on Hybrid Systems: Computation and Control, pages 221–230. ACM, 2010

    work page 2010

  37. [37]

    Sankaranarayanan, H

    S. Sankaranarayanan, H. Sipma, and Z. Manna. Constructing invariants for hybrid systems. In Proc. of HSCC 2004: the 7th Intern. Workshop on Hybrid Systems: Computation and Control, volume 2993 ofLNCS, pages 539–554. Springer, 2004

    work page 2004

  38. [38]

    Lyapunov function synthesis using handelman representations.IFAC Proceedings Volumes, 46(23):576–581, 2013

    Sriram Sankaranarayanan, Xin Chen, et al. Lyapunov function synthesis using handelman representations.IFAC Proceedings Volumes, 46(23):576–581, 2013

    work page 2013

  39. [39]

    Hypro: A C++ library of state set representations for hybrid systems reachability analysis

    Stefan Schupp, Erika Ábrahám, Ibtissem Ben Makhlouf, and Stefan Kowalewski. Hypro: A C++ library of state set representations for hybrid systems reachability analysis. InProc. of NFM 2017: the 9th International Symposium on NASA Formal Methods, volume 10227 ofLNCS, pages 288–294, 2017

    work page 2017

  40. [40]

    A method for invariant generation for polynomial continuous systems

    Andrew Sogokon, Khalil Ghorbal, Paul B Jackson, and André Platzer. A method for invariant generation for polynomial continuous systems. InProc. of VMCAI 2016: the 17th International Conference on Verification, Model Checking, and Ab- stract Interpretation, volume 9583 ofLNCS, pages 268–288. Springer, 2016

    work page 2016

  41. [41]

    A Nullstellensatz and a Positivstellensatz in semialgebraic geom- etry

    Gilbert Stengle. A Nullstellensatz and a Positivstellensatz in semialgebraic geom- etry. Mathematische Annalen, 207(2):87–97, 1974

    work page 1974

  42. [42]

    Taly and A

    A. Taly and A. Tiwari. Deductive verification of continuous dynamical systems. In FSTTCS, volume 4, pages 383–394, 2009

    work page 2009

  43. [43]

    A linear programmingrelaxationbasedapproachforgeneratingbarriercertificatesofhybrid systems

    Zhengfeng Yang, Chao Huang, Xin Chen, Wang Lin, and Zhiming Liu. A linear programmingrelaxationbasedapproachforgeneratingbarriercertificatesofhybrid systems. InInternational Symposium on Formal Methods, pages 721–738. Springer, 2016

    work page 2016