{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T14:06:30Z","timestamp":1779026790433,"version":"3.51.4"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032262196","type":"print"},{"value":"9783032262202","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T00:00:00Z","timestamp":1779062400000},"content-version":"vor","delay-in-days":137,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>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.<\/jats:p>","DOI":"10.1007\/978-3-032-26220-2_11","type":"book-chapter","created":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T13:20:39Z","timestamp":1779024039000},"page":"214-233","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Quantitative Monitoring of\u00a0Signal First-Order Logic"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1132-5516","authenticated-orcid":false,"given":"Marek","family":"Chalupa","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2985-7724","authenticated-orcid":false,"given":"Thomas A.","family":"Henzinger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-2866-8078","authenticated-orcid":false,"given":"N. Ege","family":"Sara\u00e7","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4993-773X","authenticated-orcid":false,"given":"Emily","family":"Yu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2026,5,18]]},"reference":[{"key":"11_CR1","unstructured":"PPLPY: Python interface to the parma polyhedra library. https:\/\/pypi.org\/project\/pplpy\/. Accessed 05 Dec 2025"},{"key":"11_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-642-29860-8_12","volume-title":"Runtime Verification","author":"E Asarin","year":"2012","unstructured":"Asarin, E., Donz\u00e9, A., Maler, O., Nickovic, D.: Parametric identification of temporal properties. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 147\u2013160. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-29860-8_12"},{"key":"11_CR3","first-page":"1","volume":"72","author":"R Bagnara","year":"2006","unstructured":"Bagnara, R., Hill, P.M., Zaffanella, E., Bagnara, A.: The parma polyhedra library. Sci. Comput. Program. 72, 1\u201320 (2006)","journal-title":"Sci. Comput. Program."},{"key":"11_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/978-3-030-17465-1_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Bakhirkin","year":"2019","unstructured":"Bakhirkin, A., Basset, N.: Specification and efficient monitoring beyond STL. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11428, pp. 79\u201397. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17465-1_5"},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"Bakhirkin, A., Ferr\u00e8re, T., Henzinger, T.A., Nickovic, D.: The first-order logic of signals: keynote. In: Brandenburg, B.B., Sankaranarayanan, S. (eds.) Proceedings of the International Conference on Embedded Software, EMSOFT 2018, Torino, Italy, 30 September\u20135 October 2018, p.\u00a01. IEEE (2018)","DOI":"10.1109\/EMSOFT.2018.8537203"},{"key":"11_CR6","unstructured":"Boker, U., Henzinger, T.A., Mazzocchi, N., Sara\u00e7, N.E.: Safety and liveness of quantitative automata. In: P\u00e9rez, G.A., Raskin, J.F. (eds.) 34th International Conference on Concurrency Theory, CONCUR 2023, Antwerp, Belgium, 18\u201323 September 2023, vol. 279 of LIPIcs, pp. 17:1\u201317:18. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2023)"},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"Boker, U., Henzinger, T.A., Mazzocchi, N., Sara\u00e7, N.E.: Safety and liveness of quantitative properties and automata. Log. Methods Comput. Sci. 21(2) (2025)","DOI":"10.46298\/lmcs-21(2:2)2025"},{"key":"11_CR8","doi-asserted-by":"publisher","unstructured":"Bonakdarpour, B., Momtaz, A., Nickovic, D., Sara\u00e7, N.E.: Approximate distributed monitoring under partial synchrony: balancing speed & accuracy. In: \u00c1brah\u00e1m, E., Abbas, H. (eds.) Runtime Verification - 24th International Conference, RV 2024, Istanbul, Turkey, 15\u201317 October 2024, Proceedings, vol. 15191 of Lecture Notes in Computer Science, pp. 282\u2013301. Springer, Heidelberg (2024). https:\/\/doi.org\/10.1007\/978-3-031-74234-7_18","DOI":"10.1007\/978-3-031-74234-7_18"},{"key":"11_CR9","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2020.110881","volume":"174","author":"C Boufaied","year":"2021","unstructured":"Boufaied, C., Jukss, M., Bianculli, D., Briand, L.C., Parache, Y.I.: Signal-based properties of cyber-physical systems: taxonomy and logic-based characterization. J. Syst. Softw. 174, 110881 (2021)","journal-title":"J. Syst. Softw."},{"key":"11_CR10","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1016\/j.ic.2014.01.012","volume":"236","author":"L Brim","year":"2014","unstructured":"Brim, L., Dluhos, P., Safr\u00e1nek, D., Vejpustek, T.: Stl$$ ^{\\text{* }}$$: extending signal temporal logic with signal-value freezing operator. Inf. Comput. 236, 52\u201367 (2014)","journal-title":"Inf. Comput."},{"issue":"1","key":"11_CR11","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/s10703-017-0286-7","volume":"51","author":"JV Deshmukh","year":"2017","unstructured":"Deshmukh, J.V., Donz\u00e9, A., Ghosh, S., Jin, X., Juniwal, G., Seshia, S.A.: Robust online monitoring of signal temporal logic. Formal Methods Syst. Des. 51(1), 5\u201330 (2017). https:\/\/doi.org\/10.1007\/s10703-017-0286-7","journal-title":"Formal Methods Syst. Des."},{"key":"11_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/978-3-319-11164-3_19","volume-title":"Runtime Verification","author":"A Dokhanchi","year":"2014","unstructured":"Dokhanchi, A., Hoxha, B., Fainekos, G.: On-line monitoring for temporal logic robustness. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 231\u2013246. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11164-3_19"},{"key":"11_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1007\/978-3-642-39799-8_19","volume-title":"Computer Aided Verification","author":"A Donz\u00e9","year":"2013","unstructured":"Donz\u00e9, A., Ferr\u00e8re, T., Maler, O.: Efficient robust monitoring for STL. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 264\u2013279. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_19"},{"key":"11_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/978-3-642-15297-9_9","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"A Donz\u00e9","year":"2010","unstructured":"Donz\u00e9, A., Maler, O.: Robust satisfaction of temporal logic over real-valued signals. In: Chatterjee, K., Henzinger, T.A. (eds.) FORMATS 2010. LNCS, vol. 6246, pp. 92\u2013106. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15297-9_9"},{"issue":"42","key":"11_CR15","doi-asserted-by":"publisher","first-page":"4262","DOI":"10.1016\/j.tcs.2009.06.021","volume":"410","author":"GE Fainekos","year":"2009","unstructured":"Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic specifications for continuous-time signals. Theor. Comput. Sci. 410(42), 4262\u20134291 (2009)","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"11_CR16","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/s10703-011-0114-4","volume":"38","author":"Y Falcone","year":"2011","unstructured":"Falcone, Y., Mounier, L., Fernandez, J.-C., Richier, J.-L.: Runtime enforcement monitors: composition, synthesis, and enforcement abilities. Formal Methods Syst. Des. 38(3), 223\u2013262 (2011)","journal-title":"Formal Methods Syst. Des."},{"issue":"21","key":"11_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S1474-6670(17)37044-1","volume":"33","author":"TI Fossen","year":"2000","unstructured":"Fossen, T.I.: A survey on nonlinear ship control: from theory to practice. IFAC Proc. Vol. 33(21), 1\u201316 (2000)","journal-title":"IFAC Proc. Vol."},{"key":"11_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/3-540-61576-8_77","volume-title":"Combinatorics and Computer Science","author":"K Fukuda","year":"1996","unstructured":"Fukuda, K., Prodon, A.: Double description method revisited. In: Deza, M., Euler, R., Manoussakis, I. (eds.) CCS 1995. LNCS, vol. 1120, pp. 91\u2013111. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61576-8_77"},{"key":"11_CR19","doi-asserted-by":"crossref","unstructured":"Gol, E.A.: Efficient online monitoring and formula synthesis with past STL. In: 5th International Conference on Control, Decision and Information Technologies, CoDIT 2018, Thessaloniki, Greece, 10\u201313 April 2018, pp. 916\u2013921. IEEE (2018)","DOI":"10.1109\/CoDIT.2018.8394941"},{"issue":"2","key":"11_CR20","doi-asserted-by":"publisher","first-page":"673","DOI":"10.1007\/s11334-024-00557-2","volume":"21","author":"F Gorostiaga","year":"2025","unstructured":"Gorostiaga, F., S\u00e1nchez, C.: General monitorability of totally ordered verdict domains. Innov. Syst. Softw. Eng. 21(2), 673\u2013686 (2025)","journal-title":"Innov. Syst. Softw. Eng."},{"key":"11_CR21","unstructured":"Heidlauf, P., Collins, A., Bolender, M., Bak, S.: Verification challenges in f-16 ground collision avoidance and other automated maneuvers. In: ARCH@ ADHS 2018 (2018)"},{"key":"11_CR22","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Mazzocchi, N., Sara\u00e7, N.E.: Abstract monitors for quantitative specifications. In: Dang, T., Stolz, V. (eds.) Runtime Verification - 22nd International Conference, RV 2022, Tbilisi, Georgia, 28\u201330 September 2022, Proceedings, vol. 13498 of Lecture Notes in Computer Science, pp. 200\u2013220. Springer, Heidelberg (2022)","DOI":"10.1007\/978-3-031-17196-3_11"},{"key":"11_CR23","doi-asserted-by":"publisher","unstructured":"Henzinger, T.A., Mazzocchi, N., Sara\u00e7, N.E.: Quantitative safety and liveness. In: Kupferman, O., Sobocinski, P. (eds.) Foundations of Software Science and Computation Structures - 26th International Conference, FoSSaCS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, 22\u201327 April 2023, Proceedings, vol. 13992 of Lecture Notes in Computer Science, pp. 349\u2013370. Springer, Heidelberg (2023). https:\/\/doi.org\/10.1007\/978-3-031-30829-1_17","DOI":"10.1007\/978-3-031-30829-1_17"},{"key":"11_CR24","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Sara\u00e7, N.E.: Quantitative and approximate monitoring. In: 36th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, 29 June\u20132 July 2021, pp. 1\u201314. IEEE (2021)","DOI":"10.1109\/LICS52264.2021.9470547"},{"issue":"1","key":"11_CR25","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/s10703-018-0319-x","volume":"53","author":"S Jak\u0161i\u0107","year":"2018","unstructured":"Jak\u0161i\u0107, S., Bartocci, E., Grosu, R., Nguyen, T., Ni\u010dkovi\u0107, D.: Quantitative monitoring of STL with edit distance. Formal Methods Syst. Des. 53(1), 83\u2013112 (2018). https:\/\/doi.org\/10.1007\/s10703-018-0319-x","journal-title":"Formal Methods Syst. Des."},{"issue":"2","key":"11_CR26","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/s10703-017-0276-9","volume":"51","author":"B K\u00f6nighofer","year":"2017","unstructured":"K\u00f6nighofer, B., et al.: Shield synthesis. Formal Methods Syst. Des. 51(2), 332\u2013361 (2017)","journal-title":"Formal Methods Syst. Des."},{"key":"11_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-540-30206-3_12","volume-title":"Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems","author":"O Maler","year":"2004","unstructured":"Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS\/FTRTFT -2004. LNCS, vol. 3253, pp. 152\u2013166. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30206-3_12"},{"issue":"3","key":"11_CR28","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/s10009-012-0247-9","volume":"15","author":"O Maler","year":"2013","unstructured":"Maler, O., Nickovic, D.: Monitoring properties of analog and mixed-signal circuits. Int. J. Softw. Tools Technol. Transf. 15(3), 247\u2013268 (2013)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"11","key":"11_CR29","doi-asserted-by":"publisher","first-page":"7719","DOI":"10.1109\/LRA.2023.3315536","volume":"8","author":"Y Meng","year":"2023","unstructured":"Meng, Y., Fan, C.: Signal temporal logic neural predictive control. IEEE Rob. Autom. Lett. 8(11), 7719\u20137726 (2023)","journal-title":"IEEE Rob. Autom. Lett."},{"key":"11_CR30","doi-asserted-by":"crossref","unstructured":"Menghi, C., Nejati, S., Gaaloul, K., Briand, L.C.: Generating automated and online test oracles for simulink models with continuous and uncertain behaviors. In: ESEC\/SIGSOFT FSE, pp. 27\u201338. ACM (2019)","DOI":"10.1145\/3338906.3338920"},{"key":"11_CR31","doi-asserted-by":"publisher","DOI":"10.7717\/peerj-cs.103","volume":"3","author":"A Meurer","year":"2017","unstructured":"Meurer, A., et al.: Sympy: symbolic computing in python. PeerJ Comput. Sci. 3, e103 (2017)","journal-title":"PeerJ Comput. Sci."},{"key":"11_CR32","doi-asserted-by":"crossref","unstructured":"Motzkin, T.S.,\u00a0Raiffa, H., Thompson, G.L., Thrall, R.M.: 3. The Double Description Method, pp. 51\u201374. Princeton University Press, Princeton (1953)","DOI":"10.1515\/9781400881970-004"},{"key":"11_CR33","unstructured":"Qin, Z., Zhang, K., Chen, Y., Chen, J., Fan, C.: Learning safe multi-agent control with decentralized neural barrier certificates. arXiv preprint arXiv:2101.05436 (2021)"},{"key":"11_CR34","doi-asserted-by":"publisher","unstructured":"Silvetti, S., Loreti, M., Nenzi, L.: Modular and online monitoring of temporal logic specification with integral and filter. In: K\u00f6nighofer, B., Torfah, H. (eds.) Runtime Verification - 25th International Conference, RV 2025, Graz, Austria, 15\u201319 September 2025, Proceedings, vol. 16087 of Lecture Notes in Computer Science, pp. 120\u2013139. Springer, Heidelberg (2025). https:\/\/doi.org\/10.1007\/978-3-032-05435-7_8","DOI":"10.1007\/978-3-032-05435-7_8"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-26220-2_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T13:20:41Z","timestamp":1779024041000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-26220-2_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032262196","9783032262202"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-26220-2_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"18 May 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Tokyo","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 May 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 May 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/fm-2026","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}