Quantitative monitoring of Signal First-Order logic

conference paper Quantitative monitoring of Signal First-Order logic LNCS published yes Marek Chalupa author 87e34708-d6c6-11ec-9f5b-9391e7be2463 Thomas A Henzinger author 40876CD8-F248-11E8-B48F-1D18A9856A870000-0002-2985-7724 Naci E Sarac author 8C6B42F8-C8E6-11E9-A03A-F2DCE5697425 Zhengqi Yu author 20aa2ae8-f2f1-11ed-bbfa-8205053f13420000-0002-4993-773X ToHe department FM: Formal Methods Vigilant Algorithmic Monitoring of Software project Runtime monitoring checks, during execution, whether a partial signal produced by a hybrid system satisfies its specification. Signal First-Order Logic (SFO) offers expressive real-time specifications over such signals, but currently comes only with Boolean semantics and has no tool support. We provide the first robustness-based quantitative semantics for SFO, enabling the expression and evaluation of rich real-time properties beyond the scope of existing formalisms such as Signal Temporal Logic. To enable online monitoring, we identify a past-time fragment of SFO and give a pastification procedure that transforms bounded-response SFO formulas into equisatisfiable formulas in this fragment. We then develop an efficient runtime monitoring algorithm for this past-time fragment and evaluate its performance on a set of benchmarks, demonstrating the practicality and effectiveness of our approach. To the best of our knowledge, this is the first publicly available prototype for online quantitative monitoring of full SFO. https://research-explorer.ista.ac.at/download/22006/22113/2026_LNCS_Chalupa.pdf application/pdfno Springer Nature2026Tokyo, Japan eng Signal first-order logicRobustness-based quantitative semanticsOnline runtime monitoring 27th International Symposium on Formal Methods 0302-9743 1611-3349 9783032262196 2603.0072810.1007/978-3-032-26220-2_11 16557214-233 Chalupa, M., Henzinger, T. A., Sarac, N. E., & Yu, E. (2026). Quantitative monitoring of Signal First-Order logic. In 27th International Symposium on Formal Methods (Vol. 16557, pp. 214–233). Tokyo, Japan: Springer Nature. <a href="https://doi.org/10.1007/978-3-032-26220-2_11">https://doi.org/10.1007/978-3-032-26220-2_11</a> M. Chalupa, T.A. Henzinger, N.E. Sarac, E. Yu, in:, 27th International Symposium on Formal Methods, Springer Nature, 2026, pp. 214–233. Chalupa M, Henzinger TA, Sarac NE, Yu E. 2026. Quantitative monitoring of Signal First-Order logic. 27th International Symposium on Formal Methods. FM: Formal Methods, LNCS, vol. 16557, 214–233. Chalupa, Marek, Thomas A Henzinger, Naci E Sarac, and Emily Yu. “Quantitative Monitoring of Signal First-Order Logic.” In 27th International Symposium on Formal Methods, 16557:214–33. Springer Nature, 2026. <a href="https://doi.org/10.1007/978-3-032-26220-2_11">https://doi.org/10.1007/978-3-032-26220-2_11</a>. Chalupa M, Henzinger TA, Sarac NE, Yu E. Quantitative monitoring of Signal First-Order logic. In: 27th International Symposium on Formal Methods. Vol 16557. Springer Nature; 2026:214-233. doi:<a href="https://doi.org/10.1007/978-3-032-26220-2_11">10.1007/978-3-032-26220-2_11</a> Chalupa, Marek, et al. “Quantitative Monitoring of Signal First-Order Logic.” 27th International Symposium on Formal Methods, vol. 16557, Springer Nature, 2026, pp. 214–33, doi:<a href="https://doi.org/10.1007/978-3-032-26220-2_11">10.1007/978-3-032-26220-2_11</a>. M. Chalupa, T. A. Henzinger, N. E. Sarac, and E. Yu, “Quantitative monitoring of Signal First-Order logic,” in 27th International Symposium on Formal Methods, Tokyo, Japan, 2026, vol. 16557, pp. 214–233. 220062026-06-14T22:01:44Z2026-06-22T08:21:09Z