一句话总结

TERA是一个Python原生开源框架，将连续、混合和随机系统的基于泰勒模型的可达性分析统一在单一符号-数值工作流中，克服了先前工具可扩展性有限、系统类别狭窄的局限，实现了紧致严格包络的快速原型设计，并支持随机混合系统。

核心贡献

• TERA是首个用于基于泰勒模型的可达性分析的Python原生自由开源框架，将连续、混合和连续时间随机系统统一于单一符号-数值工作流。
• TERA能够在困难的基准问题上，为非线性ODE和混合系统计算出紧致的可达集过逼近。
• TERA支持连续时间随机系统的分析，目前正在推进将基础设施扩展至随机混合系统。

引言

在受有界扰动影响的安全关键控制系统中，验证所有闭环轨迹是否保持在规定界限内需要计算前向可达集，通常通过基于集合的过逼近实现。区间和环域表示因包裹效应而产生过度保守的包络，而基于泰勒模型的方法保留了函数依赖关系并收紧界限，但现有泰勒模型工具要么依赖专有环境（MATLAB），要么缺乏对随机系统和Python生态内快速原型的支持。作者提出了TERA，这是首个完全Python原生的自由开源框架，利用泰勒模型为连续非线性ODE、混合系统和连续时间随机系统计算严格的可达集包络，并与科学Python技术栈及SageMath无缝集成。

方法

TERA使用形如$P(x_0, t) + I$P(x0​,t)+I的泰勒模型表示可达集，其中$P$P是ODE解$x(x_0, t)$x(x0​,t)的泰勒多项式逼近（取到给定阶数），$I$I是一个区间，保证真实解被包围在泰勒模型内。为实现所需的严格包络，所有区间计算均采用正确舍入，依赖通过SageMath集成的GNU MPFR库。

连续时间动态通过验证的泰勒模型积分方案进行传播。该工具支持局部单步积分，该积分建立在Berz和Makino的基础验证ODE求解方法之上，并结合了非线性连续系统的流管构造方法。为缓解在较长时间范围内产生的包裹效应，TERA采用了收缩包裹技术的组合式左右传播，迭代细化泰勒模型表示，以保持过逼近的紧致。

对于混合系统，TERA利用基于泰勒模型的混合可达性语义计算守卫交集和离散跃迁。该框架首先构建连续流管直至守卫集，然后应用基于区间的交集和重置映射，得到跃迁后可达集。

随机连续动力学的处理方式是在确定性泰勒模型流管上增加概率偏差界。遵循Jafarpour等人的方法，该工具计算$\delta$δ-概率可达集包络，保证系统轨迹以至少$1 - \delta$1−δ的概率包含在所求集合内。

实验

TERA在涵盖连续、混合和随机系统的ARCH竞赛基准测试上进行了评估。它能在几秒内为7维非线性生化网络计算出紧致的可达集包络，并可扩展至含有超越函数的高维问题。对于混合动力学，它准确捕获模式切换的流管；对于随机系统，它能计算出可靠包含蒙特卡洛采样路径的概率可达集。结果展示了TERA在多种验证任务中的通用性和有效性。