Reducing the wrapping effect in flowpipe construction using pseudo-invariants
Reducing the wrapping effect in flowpipe construction using pseudo-invariants
复制标题
使用伪不变量减少流管结构中的包裹效应
DOI：
10.1145/2593458.2593471
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Stanley Bak
中科院分区：
文献类型：
--
作者：
Stanley Bak
非线性混合自动机的可及性问题通常被分解为计算连续后继者的步骤，并处理离散过渡和重置图的步骤。在本文中，我们将展示一种可以在连续核能计算阶段减少包装效果的方法。包装效果的降低会导致误差减少和计算时间减少。
提出的方法背后的关键见解是，当计算连续后继器时，不必精确跟踪时间。我们通过引入人工不变（和相关的过渡）将混合自动机的单个模式分为一对模式，我们称之为伪不变。最终的杂化自动机是原始杂种的仿真，因此它们的确切可及态集是相同的。但是，由于通常会在离散过渡中删除时间信息，因此在构造的双仿真上运行时，用于过度应用到达的实用方法会遇到较小的包装效应误差。我们通过使用Flow*（一种最先进的可及性工具）计算非线性动力学系统的可及性来证明伪不变的方法的优势。
The reachability problem for a nonlinear hybrid automaton is often decomposed into steps where continuous successors are computed, and steps where discrete transitions and reset maps are processed. In this paper, we will show one method which can reduce the wrapping effect in the continuous-successor computation stage. A reduction in the wrapping effect can lead to both reduced error and reduced computation time.
The key insight behind the proposed method is that, when computing continuous successors, time need not be tracked precisely. We split an individual mode of a hybrid automaton into a pair of modes by introducing an artificial invariant (and associated transition) which we call a pseudo-invariant. The resultant hybrid automaton is a bisimulation of the original one, and thus their exact set of reachable states is identical. However, since time information is often dropped across discrete transitions, practical methods for overapproximating reachability can experience less wrapping-effect error when run on the constructed bisimulation. We demonstrate the advantage of the approach of pseudo-invariants by computing reachability for a nonlinear dynamical system using Flow*, a state-of-the-art reachability tool.