Implementation of Taylor models in CORA 2018
Implementation of Taylor models in CORA 2018
复制标题
泰勒模型在 CORA 2018 中的实现
DOI：
10.29007/zzc7
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Niklas Kochdumper
中科院分区：
文献类型：
--
作者：
M. Althoff;D. Grebenyuk;Niklas Kochdumper
工具表示：当函数输出的输入变量受区间限制时，计算函数输出的保证界是许多形式化方法的基本技术。由于边界函数输出的重要性，已经提出了几种方法来解决这一问题，如区间算法、仿射算法和泰勒模型。虽然所有的方法都提供了有保证的边界，但对于正式的验证工具来说，哪种方法最适合给定的问题通常是未知的。出于这个原因，我们在我们的MATLAB工具CORA中提供了上述技术的实现，以便可以快速地探索不同技术的优点和缺点，而不必编译代码。在这项工作中，我们给出了泰勒模型和仿射算法的实现；我们的区间算术实现已经发表。我们使用一组针对FLOW*和INTLAB的基准来评估我们实施的性能。据我们所知，我们还首次评估了区间算术和泰勒模型的组合性能：我们的结果表明，这种组合比只使用泰勒模型更快、更准确。
Tool Presentation: Computing guaranteed bounds of function outputs when their input variables are bounded by intervals is an essential technique for many formal methods. Due to the importance of bounding function outputs, several techniques have been proposed for this problem, such as interval arithmetic, affine arithmetic, and Taylor models. While all methods provide guaranteed bounds, it is typically unknown to a formal verification tool which approach is best suitable for a given problem. For this reason, we present an implementation of the aforementioned techniques in our MATLAB tool CORA so that advantages and disadvantages of different techniques can be quickly explored without having to compile code. In this work we present the implementation of Taylor models and affine arithmetic; our interval arithmetic implementation has already been published. We evaluate the performance of our implementation using a set of benchmarks against Flow* and INTLAB. To the best of our knowledge, we have also evaluated for the first time how a combination of interval arithmetic and Taylor models performs: our results indicate that this combination is faster and more accurate than only using Taylor models.