One-sentence Summary

TERA is a Python-native open-source framework that unifies Taylor Model-based reachability analysis for continuous, hybrid, and stochastic systems within a single symbolic-numeric workflow, overcoming the limited extensibility and narrow system classes of prior tools to enable rapid prototyping of tight rigorous enclosures and support for stochastic hybrid systems.

Key Contributions

• TERA is the first Python-native free and open-source framework for Taylor Model-based reachability analysis that unifies continuous, hybrid, and continuous-time stochastic systems within a single symbolic-numeric workflow.
• TERA computes tight reachable set overapproximations for non-linear ODEs and hybrid systems on difficult benchmark problems.
• TERA supports analysis of continuous-time stochastic systems, with ongoing work extending the infrastructure toward stochastic hybrid systems.

Introduction

In safety-critical control systems subject to bounded disturbances, verifying that all closed-loop trajectories remain within prescribed bounds requires computing forward reachable sets, typically via set-based over-approximations. Interval and zonotope representations suffer from the wrapping effect that produces excessively conservative enclosures, while Taylor Model (TM)–based methods preserve functional dependencies and tighten the bounds, yet existing TM tools either depend on proprietary environments (MATLAB) or lack support for stochastic systems and rapid prototyping within the Python ecosystem. The authors introduce TERA, the first fully Python-native free and open-source framework that leverages TMs to compute rigorous reachable-set enclosures for continuous nonlinear ODEs, hybrid systems, and continuous-time stochastic systems, seamlessly integrating with the scientific Python stack and SageMath.

Method

TERA represents reachable sets using Taylor models of the form $P(x_0, t) + I$P(x0​,t)+I, where $P$P is a Taylor polynomial approximation (up to a chosen degree) of the ODE solution $x(x_0, t)$x(x0​,t) and $I$I is an interval that guarantees the true solution is enclosed within the Taylor model. To achieve the required rigorous enclosure, all interval computations are performed with correct rounding, relying on the GNU MPFR library integrated through SageMath.

Continuous-time dynamics are propagated via validated Taylor model integration schemes. The tool supports local single-step integration that builds on the foundational validated ODE solving methods of Berz and Makino, combined with the flowpipe construction approach for non‑linear continuous systems. To mitigate the wrapping effect that arises over longer time horizons, TERA incorporates compositional left‑right propagation following the shrink‑wrapping technique, which iteratively refines the Taylor model representation to keep over‑approximation tight.

For hybrid systems, TERA computes guard intersections and discrete transitions using Taylor‑model‑based hybrid reachability semantics. The framework first forms the continuous flowpipe up to a guard set, then applies interval‑based intersection and reset mappings to obtain the post‑transition reachable set.

Stochastic continuous dynamics are handled by augmenting the deterministic Taylor model flowpipes with probabilistic deviation bounds. Following the approach of Jafarpour et al., the tool computes $\delta$δ-probabilistic reachable set enclosures, which guarantee that system trajectories stay within the computed sets with probability at least $1 - \delta$1−δ.

Experiment

TERA is evaluated on the ARCH competition benchmarks covering continuous, hybrid, and stochastic systems. It computes tight reachable set enclosures for a 7‑dimensional nonlinear biochemical network within seconds and scales to higher‑dimensional problems with transcendental functions. For hybrid dynamics, it accurately captures mode‑switching flowpipes, and for stochastic systems it computes probabilistic reachable sets that reliably contain Monte Carlo sample paths. The results demonstrate TERA’s versatility and effectiveness across a diverse range of verification tasks.