{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T14:06:34Z","timestamp":1779026794320,"version":"3.51.4"},"publisher-location":"Cham","reference-count":36,"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>Quantitative semantics of Signal Temporal Logic (STL) play an important role in both the falsification and control synthesis for dynamical systems by assigning numerical quantities to truth values. Recently, several different quantitative semantics have been proposed, offering better performance in many cases. Yet a general, systematic understanding of the structure and properties of quantitative semantics is missing. In this paper, we develop a general framework to model quantitative semantics. We focus mainly on soundness, which requires that the quantitative semantics of a statement is positive when the statement is true, and negative when the statement is false. This ensures that counterexamples will not be missed during verification. We derive simple, necessary conditions in our framework for soundness. We show how several recently proposed quantitative semantics fit in our framework, and how others do not, typically because they do not strictly satisfy soundness. We implement various quantitative semantics, including existing semantics from literature, in our framework and compare their effectiveness as objective functions for optimization-based falsification on both novel and existing benchmarks.<\/jats:p>","DOI":"10.1007\/978-3-032-26220-2_10","type":"book-chapter","created":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T13:21:30Z","timestamp":1779024090000},"page":"193-213","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A General Framework for\u00a0Robust Quantitative Semantics of\u00a0Signal Temporal Logic"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5461-6711","authenticated-orcid":false,"given":"Jiawei","family":"Chen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1576-2492","authenticated-orcid":false,"given":"Jos\u00e9 Luiz","family":"Vargas de Mendon\u00e7a","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1209-7738","authenticated-orcid":false,"given":"Konstantinos","family":"Mamouras","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6378-1447","authenticated-orcid":false,"given":"Jean-Baptiste","family":"Jeannin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2026,5,18]]},"reference":[{"key":"10_CR1","doi-asserted-by":"publisher","unstructured":"Abbas, H., Fainekos, G., Sankaranarayanan, S., Ivan\u010di\u0107, F., Gupta, A.: Probabilistic temporal logic falsification of cyber-physical systems. ACM Trans. Embed. Comput. Syst. 12(2s) (2013). https:\/\/doi.org\/10.1145\/2465787.2465797","DOI":"10.1145\/2465787.2465797"},{"key":"10_CR2","doi-asserted-by":"publisher","unstructured":"Abbas, H., Winn, A., Fainekos, G., Julius, A.A.: Functional gradient descent method for metric temporal logic specifications. In: 2014 American Control Conference, pp. 2312\u20132317. IEEE (2014). https:\/\/doi.org\/10.1109\/ACC.2014.6859453","DOI":"10.1109\/ACC.2014.6859453"},{"key":"10_CR3","doi-asserted-by":"crossref","unstructured":"Akazaki, T., Hasuo, I.: Time robustness in MTL and expressivity in hybrid system falsification. In: International Conference on Computer Aided Verification, pp. 356\u2013374. Springer (2015)","DOI":"10.1007\/978-3-319-21668-3_21"},{"key":"10_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"254","DOI":"10.1007\/978-3-642-19835-9_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y Annpureddy","year":"2011","unstructured":"Annpureddy, Y., Liu, C., Fainekos, G., Sankaranarayanan, S.: S-TaLiRo: a tool for temporal logic falsification for hybrid systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 254\u2013257. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19835-9_21"},{"key":"10_CR5","doi-asserted-by":"publisher","unstructured":"Bartocci, E., Bortolussi, L., Loreti, M., Nenzi, L.: Monitoring mobile and spatially distributed cyber-physical systems. In: Proceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design, pp. 146\u2013155. ACM, Vienna Austria (2017). https:\/\/doi.org\/10.1145\/3127041.3127050. https:\/\/dl.acm.org\/doi\/10.1145\/3127041.3127050","DOI":"10.1145\/3127041.3127050"},{"key":"10_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-319-75632-5_5","volume-title":"Lectures on Runtime Verification","author":"E Bartocci","year":"2018","unstructured":"Bartocci, E., et al.: Specification-based monitoring of cyber-physical systems: a survey on theory, tools and applications. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Verification. LNCS, vol. 10457, pp. 135\u2013175. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-75632-5_5"},{"key":"10_CR7","doi-asserted-by":"publisher","unstructured":"Cardona, G.A., Kamale, D., Vasile, C.I.: Mixed integer linear programming approach for control synthesis with weighted signal temporal logic. In: Proceedings of the 26th ACM International Conference on Hybrid Systems: Computation and Control, pp. 1\u201312. ACM, San Antonio TX USA (2023). https:\/\/doi.org\/10.1145\/3575870.3587120. https:\/\/dl.acm.org\/doi\/10.1145\/3575870.3587120","DOI":"10.1145\/3575870.3587120"},{"key":"10_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/978-3-030-60508-7_21","volume-title":"Runtime Verification","author":"A Chattopadhyay","year":"2020","unstructured":"Chattopadhyay, A., Mamouras, K.: A verified online monitor for metric temporal logic with quantitative semantics. In: Deshmukh, J., Ni\u010dkovi\u0107, D. (eds.) RV 2020. LNCS, vol. 12399, pp. 383\u2013403. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-60508-7_21"},{"key":"10_CR9","doi-asserted-by":"publisher","unstructured":"Claessen, K., Smallbone, N., Eddeland, J., Ramezani, Z., \u00c5kesson, K.: Using valued booleans to find simpler counterexamples in random testing of cyber-physical systems. IFAC-PapersOnLine 51(7), 408\u2013415 (2018). https:\/\/doi.org\/10.1016\/j.ifacol.2018.06.333. https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S2405896318306633","DOI":"10.1016\/j.ifacol.2018.06.333"},{"key":"10_CR10","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"},{"key":"10_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-642-14295-6_17","volume-title":"Computer Aided Verification","author":"A Donz\u00e9","year":"2010","unstructured":"Donz\u00e9, A.: Breach, a toolbox for verification and parameter synthesis of hybrid systems. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 167\u2013170. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_17"},{"key":"10_CR12","doi-asserted-by":"publisher","unstructured":"Eddeland, J.L., Miremadi, S., \u00c5kesson, K.: Evaluating optimization solvers and robust semantics for simulation-based falsification. In: Frehse, G., Althoff, M. (eds.) 7th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH20). EPiC Series in Computing, vol.\u00a074, pp. 259\u2013266. EasyChair (2020). https:\/\/doi.org\/10.29007\/f4vs","DOI":"10.29007\/f4vs"},{"key":"10_CR13","doi-asserted-by":"publisher","first-page":"129","DOI":"10.29007\/68dk","volume":"61","author":"G Ernst","year":"2019","unstructured":"Ernst, G., et al.: ARCH-COMP 2019 category report: falsification. EPiC Ser. Comput. 61, 129\u2013140 (2019)","journal-title":"EPiC Ser. Comput."},{"key":"10_CR14","doi-asserted-by":"publisher","unstructured":"Faella, M., Legay, A., Stoelinga, M.: Model checking quantitative linear time logic. Electron. Notes Theor. Comput. Sci. 220(3), 61\u201377 (2008). https:\/\/doi.org\/10.1016\/j.entcs.2008.11.019. https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066108004568","DOI":"10.1016\/j.entcs.2008.11.019"},{"issue":"42","key":"10_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. Theoret. Comput. Sci. 410(42), 4262\u20134291 (2009)","journal-title":"Theoret. Comput. Sci."},{"issue":"1","key":"10_CR16","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1109\/LCSYS.2020.3001875","volume":"5","author":"Y Gilpin","year":"2020","unstructured":"Gilpin, Y., Kurtz, V., Lin, H.: A smooth robustness measure of signal temporal logic for symbolic control. IEEE Control Syst. Lett. 5(1), 241\u2013246 (2020)","journal-title":"IEEE Control Syst. Lett."},{"key":"10_CR17","doi-asserted-by":"crossref","unstructured":"Haghighi, I., Mehdipour, N., Bartocci, E., Belta, C.: Control from signal temporal logic specifications with smooth cumulative quantitative semantics. In: 2019 IEEE 58th Conference on Decision and Control (CDC), pp. 4361\u20134366. IEEE (2019)","DOI":"10.1109\/CDC40024.2019.9029429"},{"key":"10_CR18","doi-asserted-by":"publisher","unstructured":"Hoxha, B., Abbas, H., Fainekos, G.: Benchmarks for temporal logic requirements for automotive systems. In: ARCH14-15. 1st and 2nd International Workshop on Applied veRification for Continuous and Hybrid Systems, pp. 25\u201318 (2015). https:\/\/doi.org\/10.29007\/xwrs. https:\/\/easychair.org\/publications\/paper\/4bfq","DOI":"10.29007\/xwrs"},{"key":"10_CR19","doi-asserted-by":"publisher","unstructured":"Jak\u0161i\u0107, S., Bartocci, E., Grosu, R., Ni\u010dkovi\u0107, D.: An algebraic framework for runtime verification. IEEE Trans. Comput.-Aided Des. Integr. Circ. Syst. 37(11), 2233\u20132243 (2018). https:\/\/doi.org\/10.1109\/TCAD.2018.2858460. https:\/\/ieeexplore.ieee.org\/document\/8493500\/","DOI":"10.1109\/TCAD.2018.2858460"},{"key":"10_CR20","doi-asserted-by":"crossref","unstructured":"Jeannin, J.B., Chen, J., de\u00a0Mendon\u00e7a, J.L.V., Mamouras, K.: Work-in-progress: towards a theory of robust quantitative semantics for signal temporal logic. In: 2022 International Conference on Embedded Software (EMSOFT), pp. 11\u201312. IEEE (2022)","DOI":"10.1109\/EMSOFT55006.2022.00013"},{"key":"10_CR21","doi-asserted-by":"publisher","unstructured":"Jha, S., Tiwari, A., Seshia, S.A., Sahai, T., Shankar, N.: TeLEx: learning signal temporal logic from positive examples using tightness metric. Formal Methods Syst. Des. 54(3), 364\u2013387 (2019). https:\/\/doi.org\/10.1007\/s10703-019-00332-1. http:\/\/link.springer.com\/10.1007\/s10703-019-00332-1","DOI":"10.1007\/s10703-019-00332-1"},{"key":"10_CR22","doi-asserted-by":"publisher","unstructured":"Jin, X., Deshmukh, J.V., Kapinski, J., Ueda, K., Butts, K.: Powertrain control verification benchmark. In: Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control, HSCC 2014, pp. 253\u2013262. Association for Computing Machinery, New York, NY, USA (2014). https:\/\/doi.org\/10.1145\/2562059.2562140","DOI":"10.1145\/2562059.2562140"},{"issue":"4","key":"10_CR23","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/BF01995674","volume":"2","author":"R Koymans","year":"1990","unstructured":"Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Syst. 2(4), 255\u2013299 (1990). https:\/\/doi.org\/10.1007\/BF01995674","journal-title":"Real-Time Syst."},{"key":"10_CR24","doi-asserted-by":"publisher","unstructured":"Leung, K., Ar\u00e9chiga, N., Pavone, M.: Backpropagation through signal temporal logic specifications: infusing logical structure into gradient-based methods. Int. J. Robot. Res. 42(6), 356\u2013370 (2023). https:\/\/doi.org\/10.1177\/02783649221082115","DOI":"10.1177\/02783649221082115"},{"key":"10_CR25","doi-asserted-by":"publisher","unstructured":"Lid\u00e9n\u00a0Eddeland, J., Claessen, K., Smallbone, N., Ramezani, Z., Miremadi, S., \u00c5kesson, K.: Enhancing temporal logic falsification with specification transformation and valued booleans. IEEE Trans. Comput.-Aided Des. Integr. Circ. Syst. 39(12), 5247\u20135260 (2020). https:\/\/doi.org\/10.1109\/TCAD.2020.2966480. https:\/\/ieeexplore.ieee.org\/document\/8957695","DOI":"10.1109\/TCAD.2020.2966480"},{"key":"10_CR26","doi-asserted-by":"publisher","unstructured":"Lindemann, L., Dimarogonas, D.V.: Robust control for signal temporal logic specifications using discrete average space robustness. Automatica 101, 377\u2013387 (2019). https:\/\/doi.org\/10.1016\/j.automatica.2018.12.022. https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0005109818306289","DOI":"10.1016\/j.automatica.2018.12.022"},{"key":"10_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"},{"key":"10_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"330","DOI":"10.1007\/978-3-030-72016-2_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K Mamouras","year":"2021","unstructured":"Mamouras, K., Chattopadhyay, A., Wang, Z.: Algebraic quantitative semantics for efficient online temporal monitoring. In: TACAS 2021. LNCS, vol. 12651, pp. 330\u2013348. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72016-2_18"},{"key":"10_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/978-3-030-88494-9_8","volume-title":"Runtime Verification","author":"K Mamouras","year":"2021","unstructured":"Mamouras, K., Chattopadhyay, A., Wang, Z.: A compositional framework for\u00a0quantitative online monitoring over\u00a0continuous-time signals. In: Feng, L., Fisman, D. (eds.) RV 2021. LNCS, vol. 12974, pp. 142\u2013163. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-88494-9_8"},{"key":"10_CR30","doi-asserted-by":"crossref","unstructured":"Mehdipour, N., Vasile, C.I., Belta, C.: Arithmetic-geometric mean robustness for control from signal temporal logic specifications. In: 2019 American Control Conference (ACC), pp. 1690\u20131695. IEEE (2019)","DOI":"10.23919\/ACC.2019.8814487"},{"key":"10_CR31","doi-asserted-by":"crossref","unstructured":"Mehdipour, N., Vasile, C.I., Belta, C.: Average-based robustness for continuous-time signal temporal logic (2019)","DOI":"10.1109\/CDC40024.2019.9029989"},{"key":"10_CR32","doi-asserted-by":"publisher","unstructured":"Nghiem, T., Sankaranarayanan, S., Fainekos, G., Ivanci\u0107, F., Gupta, A., Pappas, G.J.: Monte-Carlo techniques for falsification of temporal properties of non-linear hybrid systems. In: Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2010, pp. 211\u2013220. ACM, New York, NY, USA (2010). https:\/\/doi.org\/10.1145\/1755952.1755983","DOI":"10.1145\/1755952.1755983"},{"key":"10_CR33","doi-asserted-by":"crossref","unstructured":"Pant, Y.V., Abbas, H., Mangharam, R.: Smooth operator: control using the smooth robustness of temporal logic. In: 2017 IEEE Conference on Control Technology and Applications (CCTA), pp. 1235\u20131240. IEEE (2017)","DOI":"10.1109\/CCTA.2017.8062628"},{"key":"10_CR34","doi-asserted-by":"publisher","unstructured":"Sankaranarayanan, S., Fainekos, G.: Falsification of temporal properties of hybrid systems using the cross-entropy method. In: Proceedings of the 15th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2012, pp. 125\u2013134. ACM, New York, NY, USA (2012). https:\/\/doi.org\/10.1145\/2185632.2185653","DOI":"10.1145\/2185632.2185653"},{"key":"10_CR35","doi-asserted-by":"publisher","unstructured":"Sato, S., Waga, M., Hasuo, I.: Constrained optimization for hybrid system falsification and application to conjunctive synthesis. IFAC-PapersOnLine 54(5), 217\u2013222 (2021). https:\/\/doi.org\/10.1016\/j.ifacol.2021.08.501. https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S2405896321012763","DOI":"10.1016\/j.ifacol.2021.08.501"},{"key":"10_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"595","DOI":"10.1007\/978-3-030-81685-8_29","volume-title":"Computer Aided Verification","author":"Z Zhang","year":"2021","unstructured":"Zhang, Z., Lyu, D., Arcaini, P., Ma, L., Hasuo, I., Zhao, J.: Effective hybrid system falsification using Monte Carlo tree search guided by QB-robustness. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12759, pp. 595\u2013618. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_29"}],"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_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T13:21:33Z","timestamp":1779024093000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-26220-2_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032262196","9783032262202"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-26220-2_10","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"}}]}}