论文标题
具有时间触发过渡的参数线性混合系统的有效可及性分析
Efficient reachability analysis of parametric linear hybrid systems with time-triggered transitions
论文作者
论文摘要
有效地处理混合系统可及性的时间触发时间，可能是无确定性的开关是一项具有挑战性的任务。在本文中，我们提出了一种基于基于保守的基于集合的动力学的围墙的方法，该方法可以处理具有不确定参数和输入的系统，其中不确定性绑定到给定的间隔。该方法通过定期控制器的实验电力制动系统的植物模型进行评估。在此模型中，快速切换控制器动力学需要仿真纳米秒的时间尺度。众所周知，对于相对较大的时间范围的准确计算是昂贵的。但是，通过适当地将有关空间变量的时间变量脱在一起，并使用作用在分子台上的间隔矩阵映射封闭了不确定的参数，我们表明，相对于先前的工作，计算时间可以降低至5000倍。这是对混合系统的正式验证迈出的一步，因为降低的运行时间使工程师可以在其模型中以相对便宜的计算成本引入表现力。
Efficiently handling time-triggered and possibly nondeterministic switches for hybrid systems reachability is a challenging task. In this paper we present an approach based on conservative set-based enclosure of the dynamics that can handle systems with uncertain parameters and inputs, where the uncertainties are bound to given intervals. The method is evaluated on the plant model of an experimental electro-mechanical braking system with periodic controller. In this model, the fast-switching controller dynamics requires simulation time scales of the order of nanoseconds. Accurate set-based computations for relatively large time horizons are known to be expensive. However, by appropriately decoupling the time variable with respect to the spatial variables, and enclosing the uncertain parameters using interval matrix maps acting on zonotopes, we show that the computation time can be lowered to 5000 times faster with respect to previous works. This is a step forward in formal verification of hybrid systems because reduced run-times allow engineers to introduce more expressiveness in their models with a relatively inexpensive computational cost.
