2020/08/14 by Thomas Wright, Wright, Thomas, Ian Stark +1 · 1 citation
Computer Science · Decision Sciences · Engineering · #Embedded Systems Design Techniques #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Real-time simulation and control systems #Simulation Techniques and Applications
paper · pdf · doi:10.48550/arxiv.2008.06589
openalex publication_date 2020/08/14 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Signal Temporal Logic monitoring over numerical simulation traces has emerged\nas an effective approach to approximate verification of continuous and hybrid\nsystems. In this report we explore an exact verification procedure for STL\nproperties based on monitoring verified traces in the form of Taylor model\nflowpipes as produced by the Flow* verified integrator. We explore how tight\nintegration with Flow*'s symbolic flowpipe representation can lead to more\nprecise and more efficient monitoring. We then show how the performance of\nmonitoring can be increased substantially by introducing masks, a\nproperty-directed refinement of our method which restricts flowpipe monitoring\nto the time regions relevant to the overall truth of a complex proposition.\nFinally, we apply our implementation of these methods to verifying properties\nof a challenging continuous system, evaluating the impact of each aspect of our\nprocedure on monitoring performance.\n