TERA: A Unified Taylor Model Enabled Reachability Analysis Framework

Source: arXiv:2607.01189 · Published 2026-07-01 · By Salma Iraky, Andrew Sogokon

TL;DR

This paper presents TERA, a new Python-native open-source framework for reachability analysis of safety-critical dynamical systems using Taylor Models (TMs). Reachability analysis aims to compute rigorous enclosures of all possible system trajectories over finite time horizons to verify safety properties. Existing TM-based tools (e.g. Flow*, CORA, JuliaReach) focus on narrow system classes like deterministic ODEs or hybrid systems and are often implemented in non-Python ecosystems, limiting extensibility and rapid prototyping. TERA unifies reachability analysis for continuous nonlinear ODEs, hybrid systems, and continuous-time stochastic systems within a single symbolic-numeric Python workflow leveraging SageMath. The framework rigorously mitigates the wrapping effect by employing validated TM integration and shrink-wrapping techniques, enabling tight over-approximations of reachable sets on challenging benchmarks. Experimental validations on 7D nonlinear biochemical and hybrid bouncing ball models demonstrate accurate, computationally efficient enclosures. TERA additionally supports δ-probabilistic reachable sets for stochastic systems, marking a first in Python-based open-source TM frameworks. The authors envision further extensions to stochastic hybrid systems and neural-network-controlled systems.

Key findings

• TERA computes tight Taylor Model-based reachable set enclosures for a 7-dimensional nonlinear Laub-Loomis biochemical reaction system over time horizon [0, 20] in 13 seconds on an 8-core 3.3 GHz CPU.
• The framework handles transcendental nonlinearities (e.g., sin, cos) within ODEs, beyond polynomial-only dynamics common in some prior TM tools.
• TERA supports hybrid systems with discrete mode transitions, rigorously computing guard intersections and discrete jumps following TM hybrid reachability semantics.
• For continuous-time stochastic systems, TERA produces δ-probabilistic reachable set (δ-PRS) enclosures that contain trajectories with probability ≥ 1 − δ (δ=0.001 in example), validated by containing 2000 Euler–Maruyama Monte Carlo sample paths.
• The shrink-wrapping compositional propagation method is implemented to effectively mitigate the wrapping effect over long integration horizons.
• TERA is fully implemented in Python integrated with SageMath and GMPFR for correct rounding, enabling rapid prototyping compared to C++ (Flow*) or MATLAB (CORA) tools.
• The tool successfully benchmarks on ARCH competition problems including continuous nonlinear, hybrid, and stochastic systems.
• Current limitations include support for only continuous-time stochastic systems (no hybrid stochastic systems yet) and lack of extensive adversarial or real-world benchmarks.

Threat model

The threat model assumes uncertain disturbance or stochastic noise bounded within known intervals or distributions affecting a safety-critical dynamical system. The adversary is modeled implicitly as the uncertainty realizations, with no active malicious attacker considered. The framework targets rigorous over-approximation of all possible trajectories under these disturbances, without assumptions of adversary manipulation beyond disturbance bounds.

Methodology — deep read

1. Threat Model & Assumptions: The framework assumes an unknown but bounded disturbance or stochastic noise w in the system dynamics ˙x = f(x, κ(x), w), where x is state and u=κ(x) is control. The goal is to conservatively over-approximate all closed-loop trajectories originating from a set of initial states X0 over finite time horizon T with guaranteed enclosures. The adversary is essentially the uncertainty/disturbance realizations captured in w; no explicit attacker model is considered.

2. Data: The approach is validated on benchmark problem suites such as the ARCH COMP18 benchmarks with nonlinear biochemical and hybrid systems, and a stochastic spring example. Initial sets are defined as hyper-rectangles around initial conditions. The reachable sets are computed over specified time horizons (e.g., [0, 20] seconds). The benchmarks represent challenging nonlinearities including polynomial, transcendental functions, and hybrid discrete-continuous modes.

3. Architecture / Algorithm: The core representation uses Taylor Models of the form P(x0, t) + I, where P is a polynomial approximation of the solution trajectory and I is an interval remainder guaranteed to enclose the true solution. Continuous dynamics integration employs validated single-step TM integration methods rooted in Berz and Makino’s differential algebra techniques. To control wrapping effects, TERA implements the shrink-wrapping compositional left-right propagation method refined by Bünger. For hybrid systems, TERA computes discrete transitions and guard intersections symbolically via TM operations based on Chen’s hybrid TM reachability semantics. Stochastic dynamics are addressed via δ-probabilistic reachable sets (δ-PRS) based on recent probabilistic reachability theory [Jafarpour et al.], combining deterministic TM flowpipes with probabilistic deviation bounds to guarantee containment with high probability.

4. Training/Evaluation Regime: While not a learning method, the computation runs on standard desktop hardware with 3.3 GHz 8-core Snapdragon X Plus CPU and 16GB RAM. Computation times for the biochemical benchmark were about 13 seconds. Numerical parameters like Taylor polynomial order, step sizes, and δ values influence precision-vs-cost tradeoffs but are not detailed explicitly. Correct rounding is handled with GNU MPFR for numerical reliability.

5. Evaluation Protocol: Metrics involve tightness and rigor of reachable set enclosures visually and quantitatively on standard benchmark problems. Comparisons to prior tool results are informal as exact baselines are not re-run here. Validation of stochastic reachability is performed by verifying containment of large Monte Carlo sample trajectories inside δ-PRS bounds. No formal statistical hypothesis tests reported.

6. Reproducibility: The entire TERA framework is free and open source under GPLv2, hosted on GitHub with documentation and example benchmarks, enabling replication and extension by the community. The benchmark problems largely come from publicly available ARCH competition datasets, ensuring transparency. While frozen weights are not relevant here, the software provides a reproducible computational environment integrating symbolic and numeric methods via Python and SageMath.

Example: For the 7D Laub-Loomis biochemical network, TERA initializes the initial set as a tight hyperrectangle, computes Taylor polynomial approximations of solutions and rigorous interval remainders at each time step from [0,20]. It applies shrink-wrapping to maintain tightness of the over-approximations while propagating the flowpipes forward. The output is a set-valued enclosure illustrated in the state-space plane, computed in 13 seconds on desktop hardware.

Technical innovations

• A unified Python-native framework integrating Taylor Model-based reachability analysis for continuous, hybrid, and continuous-time stochastic systems in a single symbolic-numeric workflow.
• Implementation of compositional shrink-wrapping propagation techniques within Python to mitigate the wrapping effect and maintain tight reachable set enclosures over long horizons.
• Extension of TM-based reachability to continuous-time stochastic systems using δ-probabilistic reachable sets combining deterministic TM flowpipes with probabilistic deviation bounds, following Jafarpour et al.
• Full integration with the SageMath computer algebra system and GNU MPFR for rigorous, correctly rounded polynomial and interval arithmetic to guarantee rigor of enclosures.

Datasets

• ARCH COMP18 continuous and hybrid benchmarks — multiple nonlinear ODE and hybrid systems problems — publicly available from ARCH competition
• Stochastic spring model example from Särkkä and Solin (2019) — continuous-time stochastic system — textbook example

Baselines vs proposed

• Flow*: reported tight TM-based reachability for nonlinear ODEs in C++ (no direct runtime comparison with TERA presented)
• CORA: MATLAB toolbox for reachability (focus on deterministic/hybrid, no stochastic support; no direct comparison)
• TERA Laub-Loomis 7D biochemical model: tight enclosure in 13s on 3.3GHz 8-core CPU (baseline tool runtimes not reported for direct comparison)
• TERA stochastic δ-PRS encloses 2000 Monte Carlo paths for δ=0.001 (validating probabilistic correctness, no explicit baseline)

Figures from the paper

Figures are reproduced from the source paper for academic discussion. Original copyright: the paper authors. See arXiv:2607.01189.

Fig 1: Reachable set enclosures produced by TERA

Fig 2 (page 2).

Fig 3 (page 2).

Limitations

• Current stochastic support limited to continuous-time systems; hybrid stochastic systems not yet supported.
• No comprehensive benchmarking across all existing TM tools or baselines in terms of speed or enclosure tightness.
• Limited discussion or evaluation of numerical stability or scalability to very high-dimensional systems.
• No adversarial attack or perturbation robustness evaluation; assumed bounded disturbances with no malicious adversary.
• Reliance on symbolic-numeric backends (SageMath), which may limit performance vs. native C++ implementations in some contexts.
• Lack of detailed hyperparameter choices (e.g., Taylor order, time step size) and their impact on precision-cost tradeoffs.

Open questions / follow-ons

• How well does TERA scale to high-dimensional systems or systems with stiff dynamics beyond the presented benchmarks?
• Can the framework be extended to handle fully stochastic hybrid systems with discrete transitions under uncertainty?
• What are the tradeoffs in Taylor model order, step size, and computational cost affecting enclosure tightness and verification confidence?
• How might TERA be integrated or interfaced with neural-network controllers for reachability analysis in learned control systems?

Why it matters for bot defense

For bot-defense and CAPTCHA practitioners interested in system security verification, TERA provides a rigorous computational tool to analyze reachable states for nonlinear, hybrid, and stochastic dynamical models that might represent interactions in security-critical environments. While not directly targeted at CAPTCHAs, the framework's approach to bounding system trajectories with guaranteed enclosures could be adapted or inspire modeling of user or adversary behavior under uncertainty in automated interaction defenses. The ability to handle stochasticity with probabilistic reachable sets is especially relevant for real-world noisy systems or user behavior models. Moreover, the extensibility and Python implementation facilitate rapid prototyping of novel reachability analyses for dynamic and adaptive security controls, including potential future application to systems controlled or influenced by machine learning elements.

Cite

@article{arxiv2607_01189,
  title={ TERA: A Unified Taylor Model Enabled Reachability Analysis Framework },
  author={ Salma Iraky and Andrew Sogokon },
  journal={arXiv preprint arXiv:2607.01189},
  year={ 2026 },
  url={https://arxiv.org/abs/2607.01189}
}

Read the full paper

• arXiv:2607.01189 (abstract)
• arXiv:2607.01189 (PDF)