{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,2]],"date-time":"2026-06-02T09:26:58Z","timestamp":1780392418081,"version":"3.54.1"},"reference-count":55,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2024,3,20]],"date-time":"2024-03-20T00:00:00Z","timestamp":1710892800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,3,20]],"date-time":"2024-03-20T00:00:00Z","timestamp":1710892800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"Max Planck Institute for Software Systems (MPI-SWS)"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Innovations Syst Softw Eng"],"published-print":{"date-parts":[[2025,6]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>It is widely accepted that every system should be robust in that \u201csmall\u201d violations of environment assumptions should lead to \u201csmall\u201d violations of system guarantees, but it is less clear how to make this intuition mathematically precise. While significant efforts have been devoted to providing notions of robustness for linear temporal logic, branching-time logics, such as computation tree logic (CTL) and CTL*, have received less attention in this regard. To address this shortcoming, we develop \u201crobust\u201d extensions of CTL and CTL*, which we name robust CTL (rCTL) and robust CTL* (rCTL*). Both extensions are syntactically similar to their parent logics but employ multi-valued semantics to distinguish between \u201clarge\u201d and \u201csmall\u201d violations of the specification. We show that the multi-valued semantics of rCTL make it more expressive than CTL, while rCTL* is as expressive as CTL*. Moreover, we show that the model checking problem, the satisfiability problem, and the synthesis problem for rCTL and rCTL* have the same asymptotic complexity as their non-robust counterparts, implying that robustness can be added to branching-time logics for free.<\/jats:p>","DOI":"10.1007\/s11334-024-00552-7","type":"journal-article","created":{"date-parts":[[2024,3,20]],"date-time":"2024-03-20T21:26:16Z","timestamp":1710969976000},"page":"595-617","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Robust computation tree logic"],"prefix":"10.1007","volume":"21","author":[{"given":"Satya Prakash","family":"Nayak","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Daniel","family":"Neider","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rajarshi","family":"Roy","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Martin","family":"Zimmermann","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,3,20]]},"reference":[{"issue":"3","key":"552_CR1","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/s00236-013-0191-5","volume":"51","author":"R Bloem","year":"2014","unstructured":"Bloem R et al (2014) Synthesizing robust systems. Acta Informatica 51(3):193\u2013220. https:\/\/doi.org\/10.1007\/s00236-013-0191-5","journal-title":"Acta Informatica"},{"issue":"5","key":"552_CR2","doi-asserted-by":"publisher","first-page":"1133","DOI":"10.1109\/TAC.2008.923658","volume":"53","author":"DC Tarraf","year":"2008","unstructured":"Tarraf DC, Megretski A, Dahleh MA (2008) A framework for robust stability of systems over finite alphabets. IEEE Trans Autom Control 53(5):1133\u20131146. https:\/\/doi.org\/10.1109\/TAC.2008.923658","journal-title":"IEEE Trans Autom Control"},{"key":"552_CR3","doi-asserted-by":"crossref","unstructured":"Doyen L, Henzinger TA, Legay A, Nickovic D (2010) Robustness of sequential circuits. In: Gomes L, Khomenko V, Fernandes JM (eds) 10th international conference on application of concurrency to system design, ACSD 2010, Braga, Portugal, 21\u201325 June 2010, 77\u201384. IEEE Computer Society","DOI":"10.1109\/ACSD.2010.26"},{"key":"552_CR4","doi-asserted-by":"crossref","unstructured":"Ehlers R, Topcu U (2014) Resilience to intermittent assumption violations in reactive synthesis. In: Fr\u00e4nzle M, Lygeros J (eds) 17th international conference on hybrid systems: computation and control (part of CPS Week), HSCC\u201914, Berlin, Germany, April 15\u201317, 2014, 203\u2013212. ACM","DOI":"10.1145\/2562059.2562128"},{"issue":"12","key":"552_CR5","doi-asserted-by":"publisher","first-page":"3151","DOI":"10.1109\/TAC.2014.2351632","volume":"59","author":"P Tabuada","year":"2014","unstructured":"Tabuada P, Caliskan SY, Rungger M, Majumdar R (2014) Towards robustness for cyber-physical systems. IEEE Trans Autom Control 59(12):3151\u20133163. https:\/\/doi.org\/10.1109\/TAC.2014.2351632","journal-title":"IEEE Trans Autom Control"},{"key":"552_CR6","doi-asserted-by":"crossref","unstructured":"Tabuada P, Balkan A, Caliskan SY, Shoukry Y, Majumdar R (2012) Input\u2013output robustness for discrete systems. In: Jerraya A, Carloni LP, Maraninchi F, Regehr J (eds) Proceedings of the 12th international conference on embedded software, EMSOFT 2012, part of the eighth embedded systems week, ESWeek 2012, Tampere, Finland, October 7\u201312, 2012, 217\u2013226. ACM","DOI":"10.1145\/2380356.2380396"},{"key":"552_CR7","unstructured":"Tabuada P, Neider D (2016) Robust linear temporal logic. In: Talbot J, Regnier L (eds) 25th EACSL annual conference on computer science logic, CSL 2016, August 29\u2013September 1, 2016, Marseille, France, Vol.\u00a062 of LIPIcs, 10:1\u201310:21 (Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 2016)"},{"key":"552_CR8","doi-asserted-by":"crossref","unstructured":"Neider D, Weinert A, Zimmermann M (2019) Robust, expressive, and quantitative linear temporal logics: pick any two for free. In: Leroux J, Raskin J (eds) Proceedings tenth international symposium on games, automata, logics, and formal verification, GandALF 2019, Bordeaux, France, 2\u20133rd September 2019, Vol 305 of EPTCS, pp 1\u201316","DOI":"10.4204\/EPTCS.305.1"},{"issue":"Part","key":"552_CR9","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2021.104810","volume":"285","author":"D Neider","year":"2022","unstructured":"Neider D, Weinert A, Zimmermann M (2022) Robust, expressive, and quantitative linear temporal logics: pick any two for free. Inf Comput 285(Part):104810. https:\/\/doi.org\/10.1016\/j.ic.2021.104810","journal-title":"Inf Comput"},{"key":"552_CR10","doi-asserted-by":"publisher","unstructured":"Anevlavis T, Philippe M, Neider D, Tabuada P (2018) Verifying rLTL formulas: now faster than ever before!. In: 57th IEEE conference on decision and control, CDC 2018, Miami, FL, USA, December 17\u201319, 2018, 1556\u20131561. IEEE. https:\/\/doi.org\/10.1109\/CDC.2018.8619014","DOI":"10.1109\/CDC.2018.8619014"},{"key":"552_CR11","doi-asserted-by":"publisher","unstructured":"Anevlavis T, Neider D, Philippe M, Tabuada P (2019) Evrostos: the rLTL verifier. In: Ozay N, Prabhakar P (eds) Proceedings of the 22nd ACM international conference on hybrid systems: computation and control, HSCC 2019, Montreal, QC, Canada, April 16\u201318, 218\u2013223. ACM. https:\/\/doi.org\/10.1145\/3302504.3311812","DOI":"10.1145\/3302504.3311812"},{"issue":"2","key":"552_CR12","doi-asserted-by":"publisher","first-page":"8:1","DOI":"10.1145\/3491216","volume":"23","author":"T Anevlavis","year":"2022","unstructured":"Anevlavis T, Philippe M, Neider D, Tabuada P (2022) Being correct is not enough: efficient verification using robust linear temporal logic. ACM Trans Comput Log 23(2):8:1-8:39. https:\/\/doi.org\/10.1145\/3491216","journal-title":"ACM Trans Comput Log"},{"key":"552_CR13","doi-asserted-by":"publisher","unstructured":"Mascle C et\u00a0al (2020) From LTL to rLTL monitoring: improved monitorability through robust semantics. In: Ames AD, Seshia SA, Deshmukh J (eds) HSCC \u201920: 23rd ACM international conference on hybrid systems: computation and control, Sydney, New South Wales, Australia, April 21\u201324, 2020, 7:1\u20137:12. ACM. https:\/\/doi.org\/10.1145\/3365365.3382197","DOI":"10.1145\/3365365.3382197"},{"key":"552_CR14","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/s10703-022-00398-4","volume":"4","author":"C Mascle","year":"2022","unstructured":"Mascle C et al (2022) From LTL to rLTL monitoring: improved monitorability through robust semantics. Formal Methods Syst Des 4:5. https:\/\/doi.org\/10.1007\/s10703-022-00398-4","journal-title":"Formal Methods Syst Des"},{"key":"552_CR15","doi-asserted-by":"crossref","unstructured":"Nayak SP, Neider D, Zimmermann M (2022) Robustness-by-construction synthesis: adapting to the environment at runtime. In: Margaria T, Steffen B (eds) Leveraging applications of formal methods, verification and validation. Verification Principles, 149\u2013173. Springer, Cham","DOI":"10.1007\/978-3-031-19849-6_10"},{"key":"552_CR16","doi-asserted-by":"publisher","unstructured":"Murano A, Neider D, Zimmermann M (2023) Robust alternating-time temporal logic. In: Gaggl SA, Martinez MV, Ortiz M (eds) Logics in artificial intelligence\u201418th European conference, JELIA 2023, Dresden, Germany, September 20\u201322, 2023, Proceedings, Vol 14281 of Lecture notes in computer science, 796\u2013813. Springer. https:\/\/doi.org\/10.1007\/978-3-031-43619-2_54","DOI":"10.1007\/978-3-031-43619-2_54"},{"key":"552_CR17","doi-asserted-by":"publisher","unstructured":"Zimmermann M (2023) Robust probabilistic temporal logics. arXiv:2306.05806https:\/\/doi.org\/10.48550\/arXiv.2306.05806","DOI":"10.48550\/arXiv.2306.05806"},{"key":"552_CR18","unstructured":"French T, McCabe-Dansted JC, Reynolds M (2007) A temporal logic of robustness. In: Konev B, Wolter F (eds) Frontiers of combining systems, 6th international symposium, FroCoS 2007, Liverpool, UK, September 10\u201312, 2007, Proceedings, Vol 4720 of Lecture notes in computer science, 193\u2013205. Springer"},{"key":"552_CR19","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1016\/j.ic.2019.02.003","volume":"266","author":"J Mabe-Dansted","year":"2019","unstructured":"Mabe-Dansted J, Dixon C, French T, Reynolds M (2019) Sublogics of a branching time logic of robustness. Inf Comput 266:126\u2013160. https:\/\/doi.org\/10.1016\/j.ic.2019.02.003","journal-title":"Inf Comput"},{"key":"552_CR20","doi-asserted-by":"publisher","unstructured":"Nayak SP, Neider D, Roy R, Zimmermann M (2022) Robust computation tree logic. In: Deshmukh JV, Havelund K, Perez I (eds) NASA formal methods\u201414th international symposium, NFM 2022, Pasadena, CA, USA, May 24\u201327, 2022, Proceedings, Vol. 13260 of Lecture notes in computer science, 538\u2013556. Springer. https:\/\/doi.org\/10.1007\/978-3-031-06773-0_29","DOI":"10.1007\/978-3-031-06773-0_29"},{"key":"552_CR21","volume-title":"Principles of model checking","author":"C Baier","year":"2008","unstructured":"Baier C, Katoen J (2008) Principles of model checking. MIT Press, Cambridge"},{"key":"552_CR22","doi-asserted-by":"crossref","unstructured":"H\u00e1jek P (1998) Metamathematics of fuzzy logic Vol\u00a04 of Trends in Logic Kluwer","DOI":"10.1007\/978-94-011-5300-3"},{"issue":"2","key":"552_CR23","doi-asserted-by":"publisher","first-page":"165","DOI":"10.5007\/1808-1711.2009v13n2p165","volume":"13","author":"G Priest","year":"2009","unstructured":"Priest G (2009) Dualising intuitionictic negation. Principia Int J Epistemol 13(2):165\u2013184. https:\/\/doi.org\/10.5007\/1808-1711.2009v13n2p165","journal-title":"Principia Int J Epistemol"},{"key":"552_CR24","doi-asserted-by":"publisher","unstructured":"Dwyer MB, Avrunin GS, Corbett JC (1999) Patterns in property specifications for finite-state verification. In: Boehm BW, Garlan D, Kramer J (eds) Proceedings of the 1999 international conference on software engineering, ICSE\u2019 99, Los Angeles, CA, USA, May 16\u201322, 1999, 411\u2013420. ACM. https:\/\/doi.org\/10.1145\/302405.302672","DOI":"10.1145\/302405.302672"},{"issue":"2","key":"552_CR25","doi-asserted-by":"publisher","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"5","author":"A Tarski","year":"1955","unstructured":"Tarski A (1955) A lattice-theoretical fixpoint theorem and its applications. Pac J Math 5(2):285\u2013309","journal-title":"Pac J Math"},{"key":"552_CR26","volume-title":"Rudiments of $$\\mu $$-calculus","author":"A Arnold","year":"2001","unstructured":"Arnold A, Niwinski D (2001) Rudiments of $$\\mu $$-calculus. Elsevier, Hoboken"},{"issue":"1","key":"552_CR27","doi-asserted-by":"publisher","first-page":"43","DOI":"10.2140\/pjm.1979.82.43","volume":"82","author":"P Cousot","year":"1979","unstructured":"Cousot P, Cousot R (1979) Constructive versions of Tarski\u2019s fixed point theorems. Pac J Math 82(1):43\u201357","journal-title":"Pac J Math"},{"key":"552_CR28","unstructured":"Chatterjee K, Henzinger TA, Piterman N (2008) Algorithms for B\u00fcchi games. arXiv:0805.2620"},{"issue":"2","key":"552_CR29","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"EM Clarke","year":"1986","unstructured":"Clarke EM, Emerson EA, Sistla AP (1986) Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans Program Lang Syst 8(2):244\u2013263. https:\/\/doi.org\/10.1145\/5397.5399","journal-title":"ACM Trans Program Lang Syst"},{"key":"552_CR30","unstructured":"Schnoebelen P (2002) The complexity of temporal logic model checking. In: Balbiani P, Suzuki N, Wolter F, Zakharyaschev M (eds) Advances in modal logic 4, papers from the fourth conference on \u201cAdvances in Modal logic,\u201d held in Toulouse, France, 30 September\u20132 October 2002, 393\u2013436. King\u2019s College Publications"},{"key":"552_CR31","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D Kozen","year":"1983","unstructured":"Kozen D (1983) Results on the propositional mu-calculus. Theor Comput Sci 27:333\u2013354. https:\/\/doi.org\/10.1016\/0304-3975(82)90125-6","journal-title":"Theor Comput Sci"},{"key":"552_CR32","volume-title":"Model checking","author":"EM Clarke","year":"2018","unstructured":"Clarke EM, Grumberg O, Kroening D, Peled DA, Veith H (2018) Model checking, 2nd edn. MIT Press, Cambridge","edition":"2"},{"key":"552_CR33","doi-asserted-by":"crossref","unstructured":"Gr\u00e4del E, Thomas W, Wilke T (eds) (2002) Automata, logics, and infinite games: a guide to current research [outcome of a Dagstuhl seminar, February 2001], Vol 2500 of Lecture notes in computer science. Springer","DOI":"10.1007\/3-540-36387-4"},{"key":"552_CR34","doi-asserted-by":"publisher","first-page":"871","DOI":"10.1007\/978-3-319-10575-8_26","volume-title":"The mu-calculus and model checking","author":"J Bradfield","year":"2018","unstructured":"Bradfield J, Walukiewicz I (2018) The mu-calculus and model checking. Springer, Cham, pp 871\u2013919. https:\/\/doi.org\/10.1007\/978-3-319-10575-8_26"},{"key":"552_CR35","doi-asserted-by":"publisher","unstructured":"Emerson EA, Jutla CS (1991) Tree automata, mu-calculus and determinacy (extended abstract). In: 32nd annual symposium on foundations of computer science, San Juan, Puerto Rico, 1\u20134 October 1991, 368\u2013377. IEEE Computer Society. https:\/\/doi.org\/10.2307\/4210911109\/SFCS.1991.185392","DOI":"10.2307\/4210911109\/SFCS.1991.185392"},{"issue":"1","key":"552_CR36","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1137\/S0097539793304741","volume":"29","author":"EA Emerson","year":"1999","unstructured":"Emerson EA, Jutla CS (1999) The complexity of tree automata and logics of programs. SIAM J Comput 29(1):132\u2013158. https:\/\/doi.org\/10.1137\/S0097539793304741","journal-title":"SIAM J Comput"},{"issue":"1","key":"552_CR37","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0022-0000(85)90001-7","volume":"30","author":"EA Emerson","year":"1985","unstructured":"Emerson EA, Halpern JY (1985) Decision procedures and expressiveness in the temporal logic of branching time. J Comput Syst Sci 30(1):1\u201324. https:\/\/doi.org\/10.1016\/0022-0000(85)90001-7","journal-title":"J Comput Syst Sci"},{"issue":"3","key":"552_CR38","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1016\/0890-5401(89)90031-X","volume":"81","author":"RS Streett","year":"1989","unstructured":"Streett RS, Emerson EA (1989) An automata theoretic decision procedure for the propositional mu-calculus. Inf Comput 81(3):249\u2013264. https:\/\/doi.org\/10.1016\/0890-5401(89)90031-X","journal-title":"Inf Comput"},{"issue":"1","key":"552_CR39","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1142\/S0129054118500028","volume":"29","author":"M L\u00fcck","year":"2018","unstructured":"L\u00fcck M (2018) Quirky quantifiers: optimal models and complexity of computation tree logic. Int J Found Comput Sci 29(1):17\u201362. https:\/\/doi.org\/10.1142\/S0129054118500028","journal-title":"Int J Found Comput Sci"},{"key":"552_CR40","doi-asserted-by":"publisher","unstructured":"Kupferman O, Vardi MY (2000) $${\\mu }$$-Calculus synthesis. In: Nielsen M, Rovan B (eds) Mathematical foundations of computer science 2000, 25th international symposium, MFCS 2000, Bratislava, Slovakia, August 28\u2013September 1, 2000, Proceedings, Vol 1893 of Lecture notes in computer science, 497\u2013507. Springer. https:\/\/doi.org\/10.1007\/3-540-44612-5_45","DOI":"10.1007\/3-540-44612-5_45"},{"key":"552_CR41","unstructured":"Kupferman O, Vardi M et\u00a0al (1997) Synthesis with incomplete informatio. In: 2nd International conference on temporal logic, 91\u2013106, Manchester"},{"key":"552_CR42","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139236119","volume-title":"Temporal logics in computer science: finite-state systems. Cambridge tracts in theoretical computer science","author":"S Demri","year":"2016","unstructured":"Demri S, Goranko V, Lange M (2016) Temporal logics in computer science: finite-state systems. Cambridge tracts in theoretical computer science. Cambridge University Press, Cambridge"},{"issue":"3","key":"552_CR43","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1016\/0167-6423(87)90036-0","volume":"8","author":"EA Emerson","year":"1987","unstructured":"Emerson EA, Lei C (1987) Modalities for model checking: branching time logic strikes back. Sci Comput Program 8(3):275\u2013306. https:\/\/doi.org\/10.1016\/0167-6423(87)90036-0","journal-title":"Sci Comput Program"},{"key":"552_CR44","doi-asserted-by":"publisher","unstructured":"Pnueli A, Rosner R (1989) On the synthesis of an asynchronous reactive module. In: Ausiello G, Dezani-Ciancaglini M, Rocca SRD (eds) Automata, languages and programming, 16th international colloquium, ICALP89, Stresa, Italy, July 11\u201315, 1989, Proceedings, Vol 372 of Lecture notes in computer science, 652\u2013671. Springer. https:\/\/doi.org\/10.1007\/BFb0035790","DOI":"10.1007\/BFb0035790"},{"key":"552_CR45","doi-asserted-by":"publisher","unstructured":"Bloem R, Chockler H, Ebrahimi M, Strichman, O (2019) Synthesizing reactive systems using robustness and recovery specifications. In: Barrett CW, Yang J (eds) 2019 Formal methods in computer aided design, FMCAD 2019, San Jose, CA, USA, October 22\u201325, 2019, 147\u2013151. IEEE. https:\/\/doi.org\/10.23919\/FMCAD.2019.8894276","DOI":"10.23919\/FMCAD.2019.8894276"},{"key":"552_CR46","doi-asserted-by":"publisher","unstructured":"Rodionova A, Bartocci E, Nickovic D, Grosu R (2016) Temporal logic as filtering. In: Abate A, Fainekos G (eds) Proceedings of the 19th international conference on hybrid systems: computation and control, HSCC 2016, Vienna, Austria, April 12\u201314, 2016, 11\u201320. ACM. https:\/\/doi.org\/10.1145\/2883817.2883839","DOI":"10.1145\/2883817.2883839"},{"key":"552_CR47","doi-asserted-by":"publisher","unstructured":"Zhang C, Garlan D, Kang E (2020) A behavioral notion of robustness for software systems. In: Devanbu P, Cohen MB, Zimmermann T (eds) ESEC\/FSE \u201920: 28th ACM joint European software engineering conference and symposium on the foundations of software engineering, Virtual Event, USA, November 8\u201313, 2020, 1\u201312. ACM. https:\/\/doi.org\/10.1145\/3368089.3409753","DOI":"10.1145\/3368089.3409753"},{"key":"552_CR48","doi-asserted-by":"publisher","unstructured":"Chaudhuri S, Gulwani S, Lublinerman R (2010) Continuity analysis of programs. In: Hermenegildo MV, Palsberg J (eds) Proceedings of the 37th ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL 2010, Madrid, Spain, January 17-23, 2010, 57\u201370. ACM. https:\/\/doi.org\/10.1145\/1706299.1706308","DOI":"10.1145\/1706299.1706308"},{"key":"552_CR49","doi-asserted-by":"publisher","unstructured":"Majumdar R, Saha I (2009) Symbolic robustness analysis. In: Baker TP (ed) Proceedings of the 30th IEEE real-time systems symposium, RTSS 2009, Washington, DC, USA, 1\u20134 December 2009, 355\u2013363. IEEE Computer Society. https:\/\/doi.org\/10.1109\/RTSS.2009.17","DOI":"10.1109\/RTSS.2009.17"},{"issue":"42","key":"552_CR50","doi-asserted-by":"publisher","first-page":"4262","DOI":"10.1016\/j.tcs.2009.06.021","volume":"410","author":"G Fainekos","year":"2009","unstructured":"Fainekos G, Pappas G (2009) Robustness of temporal logic specifications for continuous-time signals. Theoret Comput Sci 410(42):4262\u20134291. https:\/\/doi.org\/10.1016\/j.tcs.2009.06.021","journal-title":"Theoret Comput Sci"},{"key":"552_CR51","doi-asserted-by":"crossref","unstructured":"Donz\u00e9 A, Maler O (2010) Robust satisfaction of temporal logic over real-valued signals. In: Chatterjee K, Henzinger TA (eds) Formal modeling and analysis of timed systems. Springer, Berlin, pp 92\u2013106","DOI":"10.1007\/978-3-642-15297-9_9"},{"key":"552_CR52","doi-asserted-by":"publisher","unstructured":"Akazaki T, Hasuo I (2015) Time robustness in MTL and expressivity in hybrid system falsification. In: Kroening D, Pasareanu CS (eds) Computer aided verification\u201427th international conference, CAV 2015, San Francisco, CA, USA, July 18\u201324, 2015, Proceedings, Part II, Vol. 9207 of Lecture notes in computer science, 356\u2013374. Springer. https:\/\/doi.org\/10.1007\/978-3-319-21668-3_21","DOI":"10.1007\/978-3-319-21668-3_21"},{"key":"552_CR53","doi-asserted-by":"publisher","unstructured":"Abbas H, Pant YV, Mangharam R (2019) Temporal logic robustness for general signal classes. In: Ozay N, Prabhakar P (eds) Proceedings of the 22nd ACM international conference on hybrid systems: computation and control, HSCC 2019, Montreal, QC, Canada, April 16\u201318, 2019, 45\u201356. ACM. https:\/\/doi.org\/10.1145\/3302504.3311817","DOI":"10.1145\/3302504.3311817"},{"key":"552_CR54","doi-asserted-by":"publisher","unstructured":"Mehdipour N, Vasile CI, Belta C (2019) Average-based robustness for continuous-time signal temporal logic. In: 58th IEEE conference on decision and control, CDC 2019, Nice, France, December 11\u201313, 2019, 5312\u20135317. IEEE. https:\/\/doi.org\/10.1109\/CDC40024.2019.9029989","DOI":"10.1109\/CDC40024.2019.9029989"},{"key":"552_CR55","doi-asserted-by":"publisher","DOI":"10.1145\/2875421","author":"S Almagor","year":"2016","unstructured":"Almagor S, Boker U, Kupferman O (2016) Formally reasoning about quality. J ACM. https:\/\/doi.org\/10.1145\/2875421","journal-title":"J ACM"}],"container-title":["Innovations in Systems and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-024-00552-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11334-024-00552-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-024-00552-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T07:05:00Z","timestamp":1750316700000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11334-024-00552-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,3,20]]},"references-count":55,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2025,6]]}},"alternative-id":["552"],"URL":"https:\/\/doi.org\/10.1007\/s11334-024-00552-7","relation":{},"ISSN":["1614-5046","1614-5054"],"issn-type":[{"value":"1614-5046","type":"print"},{"value":"1614-5054","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,3,20]]},"assertion":[{"value":"12 January 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"19 February 2024","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"20 March 2024","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors have no conflict of interest to declare that are relevant to the content of this article.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}},{"value":"Not applicable.","order":3,"name":"Ethics","group":{"name":"EthicsHeading","label":"Ethics approval"}},{"value":"Not applicable.","order":4,"name":"Ethics","group":{"name":"EthicsHeading","label":"Consent to participate"}},{"value":"Not applicable.","order":5,"name":"Ethics","group":{"name":"EthicsHeading","label":"Consent for publication"}}]}}