论文标题
技术报告：属性定向验证的信号时间逻辑监视
Technical Report: Property-Directed Verified Monitoring of Signal Temporal Logic
论文作者
论文摘要
在数值模拟轨迹上进行的信号时间逻辑监测已成为近似验证连续和混合系统的有效方法。在本报告中，我们基于由Flow*经过验证的集成器产生的Taylor Model FlowPipes的形式的监视验证的痕迹探索了STL属性的确切验证过程。我们探索与流*的符号流管表示的紧密整合可以导致更精确，更有效的监视。然后，我们展示如何通过引入口罩来大大提高监视的性能，这是我们方法的属性指导的改进，该方法将流管监视限制为与复杂命题的整体真理相关的时间区域。最后，我们将这些方法的实施应用于验证具有挑战性的连续系统的属性，评估程序的各个方面对监视性能的影响。
Signal Temporal Logic monitoring over numerical simulation traces has emerged as an effective approach to approximate verification of continuous and hybrid systems. In this report we explore an exact verification procedure for STL properties based on monitoring verified traces in the form of Taylor model flowpipes as produced by the Flow* verified integrator. We explore how tight integration with Flow*'s symbolic flowpipe representation can lead to more precise and more efficient monitoring. We then show how the performance of monitoring can be increased substantially by introducing masks, a property-directed refinement of our method which restricts flowpipe monitoring to the time regions relevant to the overall truth of a complex proposition. Finally, we apply our implementation of these methods to verifying properties of a challenging continuous system, evaluating the impact of each aspect of our procedure on monitoring performance.
