技术报告：信号时序逻辑的属性导向验证监控
Technical Report: Property-Directed Verified Monitoring of Signal Temporal Logic
摘要：
信号时序逻辑监测的数值模拟轨迹已经成为一种有效的方法来近似验证的连续和混合系统。在本报告中，我们探索了STL属性的精确验证程序，该程序基于对Flow* 验证积分器生成的泰勒模型流管形式的验证痕迹进行监控。我们将探讨与Flow* 符号流管表示的紧密集成如何实现更精确、更高效的监控。然后，我们展示了如何通过引入掩码，将流管监测限制在与复杂命题的整体真相相关的时间区域的方法的属性导向的改进来大幅提高监测的性能。最后，我们将这些方法的实现应用于验证一个具有挑战性的连续系统的属性，评估我们的程序的每个方面对监控性能的影响。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
