Lagrangian Reachtubes：下一代
Lagrangian Reachtubes: The Next Generation
摘要：
我们介绍LRT-NG，一组技术和相关的工具集，计算reachtube（在给定的时间范围内的可达状态集的过近似）的非线性动力系统。LRT-NG显著推进了最先进的Langrangian可达性及其相关工具LRT。从理论上讲，LRT-NG在三个方面优于LRT。首先，它首次使用了一个分析计算的度量的传播球，这被证明是最小化球的体积。我们强调度量计算是所有基于膨胀的技术的核心。其次，它将下一个可达集计算为两个球的交集：一个基于笛卡尔度量，另一个基于新度量。虽然这两个指标以前被认为是对立的方法，但它们的联合使用大大收紧了reachtubes。第三，它避免了“包裹效应”与有效的积分中心的可达集，通过最佳吸收的区间近似下一个球的半径。从工具开发的角度来看，LRT-NG在两方面优于LRT。首先，它是一个独立的工具，不再依赖于CAPD。这就需要使用Lohner方法和Runge-Kutta时间传播方法。其次，它有一个改进的界面，允许输入模型和初始条件作为外部输入文件提供。我们在一组全面的基准测试上进行的实验，包括两个神经ODE，证明了LRT-NG与LRT，CAPD和Flow* 相比的优越性能。
英文摘要：
We introduce LRT-NG, a set of techniques and an associated toolset that computes a reachtube (an over-approximation of the set of reachable states over a given time horizon) of a nonlinear dynamical system. LRT-NG significantly advances the state-of-the-art Langrangian Reachability and its associated tool LRT. From a theoretical perspective, LRT-NG is superior to LRT in three ways. First, it uses for the first time an analytically computed metric for the propagated ball which is proven to minimize the ball's volume. We emphasize that the metric computation is the centerpiece of all bloating-based techniques. Secondly, it computes the next reachset as the intersection of two balls: one based on the Cartesian metric and the other on the new metric. While the two metrics were previously considered opposing approaches, their joint use considerably tightens the reachtubes. Thirdly, it avoids the "wrapping effect" associated with the validated integration of the center of the reachset, by optimally absorbing the interval approximation in the radius of the next ball. From a tool-development perspective, LRT-NG is superior to LRT in two ways. First, it is a standalone tool that no longer relies on CAPD. This required the implementation of the Lohner method and a Runge-Kutta time-propagation method. Secondly, it has an improved interface, allowing the input model and initial conditions to be provided as external input files. Our experiments on a comprehensive set of benchmarks, including two Neural ODEs, demonstrates LRT-NG's superior performance compared to LRT, CAPD, and Flow*.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
