Ghorbel, Bassem, authorPrabhu, Vinayak S., authorACM, publisher2024-11-112024-11-112024-05-14Bassem Ghorbel and Vinayak S. Prabhu. 2024. Fast and Scalable Monitoring for Value-Freeze Operator augmented Signal Temporal Logic. In 27th ACM International Conference on Hybrid Systems: Computation and Control (HSCC '24), May 14–16, 2024, Hong Kong SAR, China. ACM, New York, NY, USA, 12 pages. https://doi.org/10.1145/3641513.3650128https://hdl.handle.net/10217/239544Signal Temporal Logic (STL) is a timed temporal logic formalism that has found widespread adoption for rigorous specification of properties in Cyber-Physical Systems. However, STL is unable to specify oscillatory properties commonly required in engineering design. This limitation can be overcome by the addition of additional operators, for example, signal-value freeze operators, or with first order quantification. Previous work on augmenting STL with such operators has resulted in intractable monitoring algorithms. We present the first efficient and scalable offline monitoring algorithms for STL augmented with independent freeze quantifiers. Our final optimized algorithm has a |ρ|log(|ρ|) dependence on the trace length |ρ| for most traces ρ arising in practice, and a |ρ|2 dependence in the worst case. We also provide experimental validation of our algorithms – we show the algorithms scale to traces having 100k time samples.born digitalarticleseng©Gassem Ghorbel, et al. ACM 2024. This is the author's version of the work. It is posted here for your personal use. Not for redistribution. The definitive Version of Record was published in HSCC '24, https://dx.doi.org/10.1145/3641513.3650128.signal temporal logiccyber-physical systemsalgorithmsvalue-freezingTexthttps://doi.org/10.1145/3641513.3650128