In this paper, we present an algorithm that computes funnels along trajectories of systems of ordinary differential equations. A funnel is a time-varying set of states containing the given trajectory, for which the evolution from within the set at any given time stays in the funnel. Hence it generalizes the behavior of single trajectories to sets around them, which is an important task, for example, in robot motion planning. In contrast to approaches based on sum-of-squares programming, which poorly scale to high dimensions, our approach is based on falsification and tackles the funnel computation task directly, through numerical optimization. This approach computes accurate funnel estimates far more efficiently and leaves formal verification to the end, outside all funnel size optimization loops.
翻译:在本文中,我们展示了一种算法,按照普通差分方程系统的轨迹计算漏斗。漏斗是一组包含特定轨迹的时间变化式状态,对于这些轨迹,任何特定时间在设定的轨迹的演进都停留在漏斗中。因此它概括了单轨轨轨迹围绕这些轨迹的行为,这是一个重要的任务,例如在机器人运动规划中。与基于方形总和编程的方法相比,我们的方法是以伪造为基础的,通过数字优化直接处理漏斗计算任务。这种方法计算出准确的漏斗估计效率要高得多,并将正式的核查留到最后,在所有漏斗大小优化圈之外。