{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T09:05:26Z","timestamp":1784797526771,"version":"3.55.0"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032325365","type":"print"},{"value":"9783032325372","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,7,24]],"date-time":"2026-07-24T00:00:00Z","timestamp":1784851200000},"content-version":"vor","delay-in-days":204,"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>\n                    A hard real-time system cannot miss any deadline. A weakly-hard real-time system, on the contrary, is designed to tolerate a specific number of deadline misses. For instance, the\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\texttt {{\\textbf {AnyMiss}}}\\,(2, 300)$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mrow>\n                            <mml:mi>AnyMiss<\/mml:mi>\n                            <mml:mspace\/>\n                            <mml:mo>(<\/mml:mo>\n                            <mml:mn>2<\/mml:mn>\n                            <mml:mo>,<\/mml:mo>\n                            <mml:mn>300<\/mml:mn>\n                            <mml:mo>)<\/mml:mo>\n                          <\/mml:mrow>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    weakly-hard constraint stipulates that in every window of 300 consecutive jobs, at most 2 deadlines are missed. The weakly-hard model is the state-of-the-art for industrial dependability-by-design of control systems that tolerate deterministic failures. Weakly-hard constraints correspond to regular languages. The size of the minimal finite state machine that recognizes whether a string satisfies the constraint (about 45\n                    <jats:italic>k<\/jats:italic>\n                    states for\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\texttt {{\\textbf {AnyMiss}}}\\,(2, 300)$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mrow>\n                            <mml:mi>AnyMiss<\/mml:mi>\n                            <mml:mspace\/>\n                            <mml:mo>(<\/mml:mo>\n                            <mml:mn>2<\/mml:mn>\n                            <mml:mo>,<\/mml:mo>\n                            <mml:mn>300<\/mml:mn>\n                            <mml:mo>)<\/mml:mo>\n                          <\/mml:mrow>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    ) is a notorious impediment for the verification of control system properties. This paper discusses an over-approximation of the language that allows us to provide sound safety guarantees for control systems under deadline misses that would be out of reach using the minimal finite state machine. We present a compressed language acceptor and prove that it simulates the original finite state machine. We study language cardinality properties, and report on empirical results that show how the new acceptor can be embedded in the control design workflow, leading to verifying safety for systems for which the state-of-the-art tools do not provide answers.\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-32537-2_20","type":"book-chapter","created":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T08:42:22Z","timestamp":1784796142000},"page":"409-431","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Over-Approximation of\u00a0Weakly-Hard Constraints for\u00a0Control Systems Verification"],"prefix":"10.1007","author":[{"given":"Rieke","family":"de Maeyer","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2766-9615","authenticated-orcid":false,"given":"Holger","family":"Hermanns","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1143-1127","authenticated-orcid":false,"given":"Martina","family":"Maggio","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,7,24]]},"reference":[{"key":"20_CR1","doi-asserted-by":"publisher","unstructured":"Ahrendts, L., Quinton, S., Boroske, T., Ernst, R.: Verifying weakly-hard real-time properties of traffic streams in switched networks. In: 30th Euromicro Conference on Real-Time Systems. LIPIcs, vol.\u00a0106, pp. 15:1\u201315:22. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2018). https:\/\/doi.org\/10.4230\/LIPICS.ECRTS.2018.15","DOI":"10.4230\/LIPICS.ECRTS.2018.15"},{"key":"20_CR2","doi-asserted-by":"publisher","unstructured":"Akesson, B., Nasri, M., Nelissen, G., Altmeyer, S., Davis, R.I.: An empirical survey-based study into industry practice in real-time systems. In: IEEE Real-Time Systems Symposium, pp. 3\u201311 (2020). https:\/\/doi.org\/10.1109\/RTSS49844.2020.00012","DOI":"10.1109\/RTSS49844.2020.00012"},{"key":"20_CR3","unstructured":"\u00c5str\u00f6m, K., H\u00e4gglund, T.: Advanced PID Control. ISA - The Instrumentation, Systems and Automation Society (2006)"},{"key":"20_CR4","unstructured":"\u00c5str\u00f6m, K., Wittenmark, B.: Computer-Controlled Systems: Theory and Design, Third Edition. Dover Books on Electrical Engineering, Dover Publications (2011). https:\/\/books.google.de\/books?id=9Y6D5vviqMgC"},{"key":"20_CR5","doi-asserted-by":"publisher","unstructured":"Bernat, G., Burns, A., Liamosi, A.: Weakly hard real-time systems. IEEE Trans. Comput. 50(4), 308\u2013321 (2001). https:\/\/doi.org\/10.1109\/12.919277","DOI":"10.1109\/12.919277"},{"key":"20_CR6","unstructured":"B\u00fcchi, J.R.: On a decision method in restricted second order arithmetic. In: Nagel, E., Suppes, P., Tarski, A. (eds.) Logic, Methodology and Philosophy of Science: Proceedings of the 1960 International Congress, pp. 1\u201311. Stanford University Press (1962)"},{"key":"20_CR7","doi-asserted-by":"publisher","unstructured":"Dercole, F., Della\u00a0Rossa, F.: A simple tree-based algorithm for deciding the stability of discrete-time switched linear systems. In: IEEE 56th Annual Conference on Decision and Control (CDC), pp. 5298\u20135303 (2017). https:\/\/doi.org\/10.1109\/CDC.2017.8264443","DOI":"10.1109\/CDC.2017.8264443"},{"key":"20_CR8","doi-asserted-by":"publisher","unstructured":"Gallant, M., et al.: Soft-constrained stochastic mpc of markov jump linear systems: Application to real-time control with deadline overruns. IEEE Control Systems Letters 9, 1532\u20131537 (2025). https:\/\/doi.org\/10.1109\/LCSYS.2025.3581518","DOI":"10.1109\/LCSYS.2025.3581518"},{"key":"20_CR9","doi-asserted-by":"publisher","unstructured":"Gallant, M., et al.: Structure-exploiting distributionally robust control of non-homogeneous markov jump linear systems. IEEE Control Syst. Letters 8, 3069\u20133074 (2024). https:\/\/doi.org\/10.1109\/LCSYS.2024.3520348","DOI":"10.1109\/LCSYS.2024.3520348"},{"key":"20_CR10","doi-asserted-by":"publisher","unstructured":"Gripenberg, G.: Computing the joint spectral radius. Linear Algebra and its Applications 234, 43\u201360 (1996). https:\/\/doi.org\/10.1016\/0024-3795(94)00082-4","DOI":"10.1016\/0024-3795(94)00082-4"},{"key":"20_CR11","doi-asserted-by":"publisher","unstructured":"Hammadeh, Z.A.H., Ernst, R., Quinton, S., Henia, R., Rioux, L.: Bounding deadline misses in weakly-hard real-time systems with task dependencies. In: Design, Automation & Test in Europe Conference & Exhibition, DATE, pp. 584\u2013589. IEEE (2017). https:\/\/doi.org\/10.23919\/DATE.2017.7927054","DOI":"10.23919\/DATE.2017.7927054"},{"key":"20_CR12","doi-asserted-by":"publisher","unstructured":"Hammadeh, Z.A.H., Quinton, S., Ernst, R.: Weakly-hard real-time guarantees for earliest deadline first scheduling of independent tasks. ACM Trans. Embedded Comput. Syst. 18(6), 121:1\u2013121:25 (2020). https:\/\/doi.org\/10.1145\/3356865","DOI":"10.1145\/3356865"},{"key":"20_CR13","doi-asserted-by":"publisher","unstructured":"Hertneck, M., Linsenmayer, S., Allg\u00f6wer, F.: Efficient stability analysis approaches for nonlinear weakly-hard real-time control systems. Automatica 133, 109868 (2021). https:\/\/doi.org\/10.1016\/j.automatica.2021.109868","DOI":"10.1016\/j.automatica.2021.109868"},{"key":"20_CR14","doi-asserted-by":"publisher","unstructured":"Hobbs, C., Xu, S., Ghosh, B., Fraccaroli, E., Duggirala, P.S., Chakraborty, S.: Quantitative safety-driven co-synthesis of cyber-physical system implementations. In: ACM\/IEEE 15th International Conference on Cyber-Physical Systems (ICCPS), pp. 99\u2013110 (2024). https:\/\/doi.org\/10.1109\/ICCPS61052.2024.00016","DOI":"10.1109\/ICCPS61052.2024.00016"},{"key":"20_CR15","doi-asserted-by":"publisher","unstructured":"Huang, C., Li, W., Zhu, Q.: Formal verification of weakly-hard systems. In: Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, pp. 197\u2013207. HSCC \u201919, Association for Computing Machinery, New York, NY, USA (2019). https:\/\/doi.org\/10.1145\/3302504.3311811","DOI":"10.1145\/3302504.3311811"},{"key":"20_CR16","doi-asserted-by":"publisher","unstructured":"Jungers, R.: The joint spectral radius: theory and applications, vol.\u00a0385. Springer Science & Business Media (2009). https:\/\/doi.org\/10.1007\/978-3-540-95980-9","DOI":"10.1007\/978-3-540-95980-9"},{"key":"20_CR17","doi-asserted-by":"publisher","unstructured":"Kirsch, C.M., Sokolova, A.: The Logical Execution Time Paradigm, pp. 103\u2013120. Advances in Real-Time Systems, Springer Berlin Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24349-3_5","DOI":"10.1007\/978-3-642-24349-3_5"},{"key":"20_CR18","doi-asserted-by":"publisher","unstructured":"Kupferman, O.: Automata theory and model checking. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 107\u2013151. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_4","DOI":"10.1007\/978-3-319-10575-8_4"},{"key":"20_CR19","doi-asserted-by":"publisher","unstructured":"Larsen, K.G., Schilling, C., Srba, J.: Simulation relations and applications in formal methods. In: Raskin, J., Chatterjee, K., Doyen, L., Majumdar, R. (eds.) Principles of Systems Design - Essays Dedicated to Thomas A. Henzinger on the Occasion of His 60th Birthday. Lecture Notes in Computer Science, vol. 13660, pp. 272\u2013291. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-22337-2_13","DOI":"10.1007\/978-3-031-22337-2_13"},{"key":"20_CR20","doi-asserted-by":"publisher","unstructured":"Linsenmayer, S., Allg\u00f6wer, F.: Stabilization of networked control systems with weakly hard real-time dropout description. In: IEEE Annual Conference on Decision and Control, pp. 4765\u20134770. IEEE (2017). https:\/\/doi.org\/10.1109\/CDC.2017.8264364","DOI":"10.1109\/CDC.2017.8264364"},{"key":"20_CR21","doi-asserted-by":"publisher","unstructured":"Rieke\u00a0de Maeyer, Holger\u00a0Hermanns, M.M.: Over-approximation of weakly-hard constraints for control systems verification (extended) (2026). https:\/\/doi.org\/10.48550\/arXiv.2605.16959","DOI":"10.48550\/arXiv.2605.16959"},{"key":"20_CR22","doi-asserted-by":"publisher","unstructured":"Maggio, M., Hamann, A., Mayer-John, E., Ziegenbein, D.: Control-system stability under consecutive deadline misses constraints. In: Euromicro Conference on Real-Time Systems. LIPIcs, vol.\u00a0165, pp. 21:1\u201321:24. Schloss Dagstuhl\u2013Leibniz-Zentrum f\u00fcr Informatik (2020). https:\/\/doi.org\/10.4230\/LIPIcs.ECRTS.2020.21","DOI":"10.4230\/LIPIcs.ECRTS.2020.21"},{"key":"20_CR23","unstructured":"Park, D.: Concurrency and automata on infinite sequences. Theory of Computation Report 104(35) (1981), department of Computer Science, University of Warwick"},{"key":"20_CR24","doi-asserted-by":"publisher","unstructured":"Pazzaglia, P., Pannocchi, L., Biondi, A., Di\u00a0Natale, M.: Beyond the weakly hard model: Measuring the performance cost of deadline misses. In: 30th Euromicro Conference on Real-Time Systems. Leibniz International Proceedings in Informatics, vol.\u00a0106, pp. 10:1\u201310:22. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2018). https:\/\/doi.org\/10.4230\/LIPIcs.ECRTS.2018.10","DOI":"10.4230\/LIPIcs.ECRTS.2018.10"},{"key":"20_CR25","doi-asserted-by":"publisher","unstructured":"Philippe, M., Essick, R., Dullerud, G.E., Jungers, R.M.: Stability of discrete-time switching systems with constrained switching sequences. Automatica 72, 242\u2013250 (2016). https:\/\/doi.org\/10.1016\/j.automatica.2016.05.015, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S000510981630200X","DOI":"10.1016\/j.automatica.2016.05.015"},{"key":"20_CR26","doi-asserted-by":"crossref","unstructured":"Rota, G.C., Strang, G.: A note on the joint spectral radius. Indag. Math 22(4), 379\u2013381 (1960)","DOI":"10.1016\/S1385-7258(60)50046-1"},{"key":"20_CR27","doi-asserted-by":"publisher","unstructured":"Seidel, M., Lang, S., Allg\u00f6wer, F.: On $$\\ell $$2-performance of weakly-hard real-time control systems. Europ. J. Contr. 80, 101056 (2024). https:\/\/doi.org\/10.1016\/j.ejcon.2024.101056, 2024 European","DOI":"10.1016\/j.ejcon.2024.101056"},{"key":"20_CR28","unstructured":"Seneta, E.: Non-negative Matrices and Markov Chains, Second Edition. Springer New York, New York, NY, USA (2006)"},{"key":"20_CR29","doi-asserted-by":"publisher","unstructured":"Vardi, M.Y.: Automata-theoretic techniques for temporal reasoning. In: Blackburn, P., van Benthem, J.F.A.K., Wolter, F. (eds.) Handbook of Modal Logic, Studies in logic and practical reasoning, vol.\u00a03, pp. 971\u2013989. North-Holland (2007). https:\/\/doi.org\/10.1016\/S1570-2464(07)80020-6","DOI":"10.1016\/S1570-2464(07)80020-6"},{"key":"20_CR30","doi-asserted-by":"publisher","unstructured":"Vreman, N., Cervin, A., Maggio, M.: Stability and performance analysis of control systems subject to bursts of deadline misses. In: Euromicro Conference on Real-Time Systems. LIPIcs, vol.\u00a0196, pp. 15:1\u201315:23. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021). https:\/\/doi.org\/10.4230\/LIPIcs.ECRTS.2021.15","DOI":"10.4230\/LIPIcs.ECRTS.2021.15"},{"key":"20_CR31","doi-asserted-by":"publisher","unstructured":"Vreman, N., Pates, R., Maggio, M.: WeaklyHard.jl: Scalable analysis of weakly-hard constraints. In: IEEE 28th Real-Time and Embedded Technology and Applications Symposium, pp. 228\u2013240 (2022). https:\/\/doi.org\/10.1109\/RTAS54340.2022.00026","DOI":"10.1109\/RTAS54340.2022.00026"},{"key":"20_CR32","doi-asserted-by":"publisher","unstructured":"Vreman, N., Pates, R., Maggio, M.: Weaklyhard.jl: Scalable analysis of weakly-hard constraints. In: IEEE Real-Time and Embedded Technology and Applications Symposium, pp. 228\u2013240. IEEE (2022). https:\/\/doi.org\/10.1109\/RTAS54340.2022.00026","DOI":"10.1109\/RTAS54340.2022.00026"},{"key":"20_CR33","doi-asserted-by":"publisher","unstructured":"Vreman, N., Pazzaglia, P., Magron, V., Wang, J., Maggio, M.: Stability of linear systems under extended weakly-hard constraints. IEEE Contr. Syst. Lett. 6, 2900\u20132905 (2022). https:\/\/doi.org\/10.1109\/LCSYS.2022.3179960","DOI":"10.1109\/LCSYS.2022.3179960"},{"key":"20_CR34","doi-asserted-by":"publisher","unstructured":"Xu, S., Ghosh, B., Hobbs, C., Thiagarajan, P.S., Chakraborty, S.: Safety-aware flexible schedule synthesis for cyber-physical systems using weakly-hard constraints. In: Proceedings of the 28th Asia and South Pacific Design Automation Conference, pp. 46\u201351. ASPDAC, Association for Computing Machinery, New York, NY, USA (2023). https:\/\/doi.org\/10.1145\/3566097.3567848","DOI":"10.1145\/3566097.3567848"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-32537-2_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T08:42:26Z","timestamp":1784796146000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-32537-2_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032325365","9783032325372"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-32537-2_20","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":"24 July 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","label":"Disclosure of Interests","group":{"name":"EthicsHeading","label":"Ethics"}},{"value":"The code for the experiments presented in this paper is available at\n                      \n                      .","order":2,"name":"Ethics","label":"Data-Availability Statement","group":{"name":"EthicsHeading","label":"Ethics"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","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":"26 July 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 July 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"38","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.floc26.org\/program","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}