This paper concerns the verification of continuous-time polynomial spline trajectories against linear temporal logic specifications (LTL without 'next'). Each atomic proposition is assumed to represent a state space region described by a multivariate polynomial inequality. The proposed approach samples a trajectory strategically, to capture every one of its region transitions. This yields a discrete word called a trace, which is amenable to established formal methods for path checking. The original continuous-time trajectory is shown to satisfy the specification if and only if its trace does. General topological conditions on the sample points are derived that ensure a trace is recorded for arbitrary continuous paths, given arbitrary region descriptions. Using techniques from computer algebra, a trace generation algorithm is developed to satisfy these conditions when the path and region boundaries are defined by polynomials. The proposed PolyTrace algorithm has polynomial complexity in the number of atomic propositions, and is guaranteed to produce a trace of any polynomial path. Its performance is demonstrated via numerical examples and a case study from robotics.
翻译:本文涉及根据线性时间逻辑规格( LTL 不含“ 下一步 ” ) 校验连续时间多球样条轨迹的核查。 假设每个原子主张代表多变量多元不平等所描述的国家空间区域。 提议的方法从战略角度对轨迹进行取样, 以捕捉每个区域过渡过程。 这产生一个叫“ 痕量” 的单词, 这符合既定的正规路径检查方法。 原始的连续时间轨迹只有在其痕量达到时才能显示为符合规格。 样点的一般地貌条件是, 确保任意连续路径的踪迹记录, 并给出任意的区域描述。 使用计算机代数技术, 开发一种痕量生成算法, 在多数值参数界定路径和区域边界时满足这些条件。 拟议的聚合轨迹算法在原子主张数量上具有多数值的复杂性, 并保证产生任何多球路径的痕迹。 其表现通过数字示例和机器人的案例研究得到证明。