pith. sign in

arxiv: 2605.16959 · v1 · pith:X23JI236new · submitted 2026-05-16 · 📡 eess.SY · cs.FL· cs.SY

Over-approximation of weakly-hard constraints for control systems verification (Extended)

Rieke de Maeyer , Holger Hermanns , Martina Maggio This is my paper

Pith reviewed 2026-05-19 20:10 UTC · model grok-4.3

classification 📡 eess.SY cs.FLcs.SY
keywords weakly-hard constraintsdeadline missescontrol systems verificationover-approximationfinite state machineslanguage acceptancesafety guaranteesreal-time systems
0
0 comments X

The pith

A compressed language acceptor over-approximates weakly-hard deadline-miss constraints while simulating the original finite-state machine, enabling safety verification for control systems where exact models are too large.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

Weakly-hard constraints let control systems tolerate a bounded number of deadline misses inside sliding windows, such as at most two misses in any 300 consecutive jobs. The minimal automaton that recognizes whether a job sequence obeys such a constraint can reach tens of thousands of states, blocking standard verification tools. The paper replaces this automaton with a smaller over-approximating acceptor, proves that the new machine simulates every accepting run of the original, and shows that the resulting safety certificates remain sound for the real system. Empirical embedding of the acceptor into a control-design loop demonstrates that previously intractable safety questions now receive answers.

Core claim

The central claim is that an explicitly constructed compressed language acceptor recognizes an over-approximation of any weakly-hard constraint language, that this acceptor simulates the minimal finite-state machine for the exact constraint, and that the smaller machine can therefore be substituted into existing verification pipelines to obtain sound safety guarantees for plants subject to deadline misses.

What carries the argument

The compressed language acceptor, a finite-state machine that over-approximates the regular language of a weakly-hard constraint while preserving simulation of the original minimal automaton.

If this is right

  • Safety verification becomes feasible for plants whose exact weakly-hard automata exceed the capacity of current model checkers.
  • Sound (conservative) certificates replace the previous all-or-nothing situation in which no answer could be obtained.
  • Language-cardinality results quantify how much extra behavior the over-approximation admits.
  • The same acceptor can be reused across multiple controller designs that share the same weakly-hard specification.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Designers could iterate between controller synthesis and the compressed acceptor to tighten the over-approximation on demand.
  • The technique may extend to other regular constraints that appear in scheduling or fault-tolerance analysis.
  • If the cardinality gap remains small, the acceptor could also support probabilistic or statistical verification methods that sample from the over-approximated language.

Load-bearing premise

The over-approximation must stay tight enough that the safety properties it certifies are non-vacuous for the concrete control systems under study.

What would settle it

A control system for which the compressed acceptor certifies closed-loop safety yet an exhaustive simulation under the exact AnyMiss(2,300) constraint reveals a deadline-miss sequence that drives the plant into an unsafe state.

Figures

Figures reproduced from arXiv: 2605.16959 by Holger Hermanns, Martina Maggio, Rieke de Maeyer.

Figure 1
Figure 1. Figure 1: Example: Automaton A2,5 corresponding to AnyMiss (2, 5). Definition 3.2 (g: index of the i-th last zero in v). Function g : V ×N + → N + ∪ {∞} gives the index of the i-th last zero in v, or infinity when no such instance exists. g(vs:1, i) := ( ∞ Ps j=1(1 − vj ) < i minp Pp j=1(1 − vj ) = i otherwise (4) For example, for v = v9:1 = 100111010, we have g(v, 1) = 1, g(v, 2) = 3, g(v, 3) = 7, g(v, 4) = 8 and g… view at source ↗
Figure 2
Figure 2. Figure 2: Example: Automaton H2,5 for AnyMiss (2, 5). We have now shown that we can construct an equivalent automaton Hm,k, that includes information that will be used for the compression introduced in the following. An example of the construction is given in [PITH_FULL_IMAGE:figures/full_fig_p008_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Example: T2,5,3 for Trim (2, 5, 3). Definition 3.8 (Compressed automaton). We define the compressed au￾tomaton Tm,k,c = (Uc, Fc) as Uc = {⟨u1, . . . , um⟩ | 0 ≤ ui ≤ k − m ∧ ui ≥ uj for i < j ∧ ((u1 − u2) mod c = 0 or um = 0)}, Fc = {(⟨u1 . . . , um⟩, 1,⟨max(u1 − 1, 0), . . . , max(um − 1, 0)⟩) | u ∈ Uc} ∪ {(⟨u1, . . . , um⟩, 0,⟨u0, u1, . . . , um−1⟩) | u ∈ Uc ∧ um = 0 ∧ u0 = ( k − m if um−1 = 0 k − m − (k… view at source ↗
Figure 4
Figure 4. Figure 4: Illustration of the size of Trim (2, 300, c) when c ∈ [100, 300]. Remark 3.14. Since we are interested in relatively large values of k and small values of m, the above result is powerful, even though the size is lower bounded by k−1 m−1  which appears not far off from k m  . Taking AnyMiss (2, 300) as an example, we see that 300 2  = 44 850 while 299 1  = 299. This compares favor￾ably to the other know… view at source ↗
Figure 5
Figure 5. Figure 5: Illustration of the language cardinality growths for increasing word length. 4.2 Comparing Am,k and Tm,k,c We now focus on RQ2, asking if our method is more efficient than using the classic weakly-hard framework, and if so by what magnitude. We choose the constraint AnyMiss (2, 50) and its compression Trim (2, 50, 45). The reason to choose in particular this constraint and this trim is that we expect that … view at source ↗
Figure 6
Figure 6. Figure 6: Illustration of the space needed for Trim (2, 300, c) when c ∈ [100, 300] with system #8 from [PITH_FULL_IMAGE:figures/full_fig_p018_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Illustration of the possible values for u2 when m = 2. (iii) The last case m > 2. In this case we further split the set Uc,critical into the disjoint subsets Uc,critical,d Uc,critical = [˙ d∈{0,...,k−m−1} Uc,critical,d, (19) based on the difference d between the second and the last element of each tuple, obtaining Uc,critical,d = {⟨u1, . . . , um⟩ | u ∈ Uc,critical and u2 − um = d}. (20) We briefly justify… view at source ↗
Figure 8
Figure 8. Figure 8: Illustration of the possible values for u1 when m > 2. Rewriting the condition d = u2 − um, leads to d = (u2 − u3) + (u3 − u4) + · · · + (um−1 − um) = Xm i=3 ui−1 − ui . (26) The requirement for the values u3, . . . , um−1 stated in (25) is equivalent to each summand of this sum being greater than or equal to zero, i.e., ui−1 − ui ≥ 0. Defining di = ui−1 − ui , we obtain d = Xm i=3 di where di ∈ N. (27) Th… view at source ↗
read the original abstract

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 AnyMiss(2, 300) 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 45k states for AnyMiss(2, 300)) 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper introduces an over-approximation technique for weakly-hard real-time constraints (e.g., AnyMiss(2,300)) in control-system verification. It replaces the minimal FSM (approximately 45k states) with a smaller compressed language acceptor, proves that the acceptor simulates the original machine (ensuring language inclusion and thus sound safety guarantees), studies cardinality properties of the accepted languages, and reports empirical results showing successful embedding into control-design workflows where state-of-the-art tools fail to return answers.

Significance. If the over-approximation remains sufficiently tight, the work would meaningfully expand the set of control systems for which safety under deadline misses can be formally verified. The simulation proof supplies soundness, and the reported empirical embedding demonstrates practical reach beyond current tools. The significance is tempered by the need for explicit evidence that the enlarged language does not render safety properties vacuous in closed-loop settings.

major comments (2)
  1. [Section 5 (empirical evaluation) and Section 4 (cardinality properties)] The central claim that the compressed acceptor yields useful (non-vacuous) safety guarantees rests on the tightness of the over-approximation. The manuscript studies language cardinality but does not report quantitative bounds on the ratio of accepted strings or the additional miss patterns admitted relative to the original FSM; without such metrics it is impossible to assess whether the safety results obtained in the empirical section remain informative rather than trivially true.
  2. [Section 3 (compressed acceptor and simulation proof)] The simulation proof (presumably Theorem 1 or equivalent in the section presenting the compressed acceptor) establishes language inclusion, but the argument does not address whether the compression preserves the periodic-window structure of AnyMiss(k,n) constraints tightly enough for the subsequent control-verification step; a concrete counter-example sequence or tightness lemma would strengthen the load-bearing claim.
minor comments (2)
  1. [Section 3] Notation for the compressed acceptor states and transition relation should be introduced with an explicit small example (e.g., AnyMiss(1,5)) before the general construction to improve readability.
  2. [Section 2] The abstract states that the minimal FSM for AnyMiss(2,300) has 'about 45k states'; the exact number and the construction method used to obtain it should be cited or reproduced in the preliminaries.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive comments, which help clarify the presentation of the over-approximation's properties and its utility in control-system verification. We respond to each major comment below and indicate the revisions we will make.

read point-by-point responses

  1. Referee: [Section 5 (empirical evaluation) and Section 4 (cardinality properties)] The central claim that the compressed acceptor yields useful (non-vacuous) safety guarantees rests on the tightness of the over-approximation. The manuscript studies language cardinality but does not report quantitative bounds on the ratio of accepted strings or the additional miss patterns admitted relative to the original FSM; without such metrics it is impossible to assess whether the safety results obtained in the empirical section remain informative rather than trivially true.

    Authors: We agree that explicit quantitative measures of tightness would allow readers to better judge whether the obtained safety results are informative. The manuscript already examines cardinality properties of the languages accepted by the original FSM and the compressed acceptor. In the revision we will augment Section 4 with concrete ratios (number of accepted strings of bounded length for representative AnyMiss(k,n) instances) and will list a small set of additional miss patterns admitted only by the compressed acceptor. These metrics will be cross-referenced with the control-design examples in Section 5 to show that the safety properties verified remain non-vacuous. revision: yes

  2. Referee: [Section 3 (compressed acceptor and simulation proof)] The simulation proof (presumably Theorem 1 or equivalent in the section presenting the compressed acceptor) establishes language inclusion, but the argument does not address whether the compression preserves the periodic-window structure of AnyMiss(k,n) constraints tightly enough for the subsequent control-verification step; a concrete counter-example sequence or tightness lemma would strengthen the load-bearing claim.

    Authors: The simulation relation is proved to guarantee language inclusion, which directly supplies the soundness argument required for safety verification: any property shown to hold under the larger language also holds under the original AnyMiss language. The compression merges states whose future acceptance behavior is identical with respect to the window constraints; this preserves the essential periodic structure while reducing the state space. To address the request for illustration, the revised Section 3 will include an explicit counter-example sequence accepted by the compressed acceptor but rejected by the minimal FSM, together with a short discussion of how the deviation in missed deadlines remains bounded within each window. A dedicated tightness lemma is not required for soundness but will be added if space permits. revision: partial

Circularity Check

0 steps flagged

No circularity; independent construction and proof of simulation

full rationale

The derivation constructs an explicit compressed acceptor, proves simulation of the original FSM via language inclusion (a standard automata-theoretic argument), studies cardinality properties as a separate analysis, and validates embedding through empirical results on control systems. These steps do not reduce to self-definition, fitted inputs renamed as predictions, or load-bearing self-citations. The over-approximation is sound by construction for safety guarantees, with tightness evaluated externally rather than forced internally. The paper is self-contained against the stated benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Review performed on abstract only; no free parameters, axioms, or invented entities are identifiable.

pith-pipeline@v0.9.0 · 5754 in / 990 out tokens · 34224 ms · 2026-05-19T20:10:50.998774+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

37 extracted references · 37 canonical work pages

  1. [1]

    Verifying weakly-hard real-time properties of traffic streams in switched networks

    Leonie Ahrendts, Sophie Quinton, Thomas Boroske, and Rolf Ernst. Verifying weakly-hard real-time properties of traffic streams in switched networks. In30th Euromicro Conference on Real-Time Systems, volume 106 ofLIPIcs, pages 15:1– 15:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018

    work page 2018

  2. [2]

    Benny Akesson, Mitra Nasri, Geoffrey Nelissen, Sebastian Altmeyer, and Robert I. Davis. An empirical survey-based study into industry practice in real-time systems. InIEEE Real-Time Systems Symposium, pages 3–11, 2020

    work page 2020

  3. [3]

    ISA - The Instru- mentation, Systems and Automation Society, 2006

    Karl Johan Åström and Tore Hägglund.Advanced PID Control. ISA - The Instru- mentation, Systems and Automation Society, 2006

    work page 2006

  4. [4]

    Åström and B

    K.J. Åström and B. Wittenmark.Computer-Controlled Systems: Theory and De- sign, Third Edition. Dover Books on Electrical Engineering. Dover Publications, 2011

    work page 2011

  5. [5]

    Bernat, A

    G. Bernat, A. Burns, and A. Liamosi. Weakly hard real-time systems.IEEE Transactions on Computers, 50(4):308–321, 2001

    work page 2001

  6. [6]

    Richard Büchi

    J. Richard Büchi. On a decision method in restricted second order arithmetic. In Ernest Nagel, Patrick Suppes, and Alfred Tarski, editors,Logic, Methodology and Philosophy of Science: Proceedings of the 1960 International Congress, pages 1–11. Stanford University Press, 1962. 20 Rieke de Maeyer, Holger Hermanns , Martina Maggio

    work page 1960

  7. [7]

    A simple tree-based algorithm for decid- ing the stability of discrete-time switched linear systems

    Fabio Dercole and Fabio Della Rossa. A simple tree-based algorithm for decid- ing the stability of discrete-time switched linear systems. InIEEE 56th Annual Conference on Decision and Control (CDC), pages 5298–5303, 2017

    work page 2017

  8. [8]

    Structure-exploiting distribu- tionally robust control of non-homogeneous markov jump linear systems.IEEE Control Systems Letters, 8:3069–3074, 2024

    Melanie Gallant, Christoph Mark, Paolo Pazzaglia, Johannes von Keler, Laura Beermann, Kevin Schmidt, and Martina Maggio. Structure-exploiting distribu- tionally robust control of non-homogeneous markov jump linear systems.IEEE Control Systems Letters, 8:3069–3074, 2024

    work page 2024

  9. [9]

    Soft-constrained stochastic mpc of markov jump linear systems: Application to real-time control with deadline overruns.IEEE Control Systems Letters, 9:1532–1537, 2025

    Melanie Gallant, Christoph Mark, Paolo Pazzaglia, Johannes von Keler, Laura Beermann, Kevin Schmidt, and Martina Maggio. Soft-constrained stochastic mpc of markov jump linear systems: Application to real-time control with deadline overruns.IEEE Control Systems Letters, 9:1532–1537, 2025

    work page 2025

  10. [10]

    Computing the joint spectral radius.Linear Algebra and its Applications, 234:43–60, 1996

    Gustaf Gripenberg. Computing the joint spectral radius.Linear Algebra and its Applications, 234:43–60, 1996

    work page 1996

  11. [11]

    Bounding deadline misses in weakly-hard real-time systems with task dependencies

    Zain Alabedin Haj Hammadeh, Rolf Ernst, Sophie Quinton, Rafik Henia, and Lau- rent Rioux. Bounding deadline misses in weakly-hard real-time systems with task dependencies. InDesign, Automation & Test in Europe Conference & Exhibition, DATE, pages 584–589. IEEE, 2017

    work page 2017

  12. [12]

    Weakly-hard real- time guarantees for earliest deadline first scheduling of independent tasks.ACM Transactions on Embedded Computing Systems, 18(6):121:1–121:25, 2020

    Zain Alabedin Haj Hammadeh, Sophie Quinton, and Rolf Ernst. Weakly-hard real- time guarantees for earliest deadline first scheduling of independent tasks.ACM Transactions on Embedded Computing Systems, 18(6):121:1–121:25, 2020

    work page 2020

  13. [13]

    Efficient stability analysis approaches for nonlinear weakly-hard real-time control systems.Auto- matica, 133:109868, 2021

    Michael Hertneck, Steffen Linsenmayer, and Frank Allgöwer. Efficient stability analysis approaches for nonlinear weakly-hard real-time control systems.Auto- matica, 133:109868, 2021

    work page 2021

  14. [14]

    Quantitative safety-driven co-synthesis of cyber- physical system implementations

    Clara Hobbs, Shengjie Xu, Bineet Ghosh, Enrico Fraccaroli, Parasara Sridhar Dug- girala, and Samarjit Chakraborty. Quantitative safety-driven co-synthesis of cyber- physical system implementations. InACM/IEEE 15th International Conference on Cyber-Physical Systems (ICCPS), pages 99–110, 2024

    work page 2024

  15. [15]

    Formal verification of weakly-hard systems

    Chao Huang, Wenchao Li, and Qi Zhu. Formal verification of weakly-hard systems. InProceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, HSCC ’19, page 197–207, New York, NY, USA, 2019. Association for Computing Machinery

    work page 2019

  16. [16]

    Springer Science & Business Media, 2009

    Raphaël Jungers.The joint spectral radius: theory and applications, volume 385. Springer Science & Business Media, 2009

    work page 2009

  17. [17]

    Kirsch and Ana Sokolova.The Logical Execution Time Paradigm, pages 103–120

    Christoph M. Kirsch and Ana Sokolova.The Logical Execution Time Paradigm, pages 103–120. Advances in Real-Time Systems. Springer Berlin Heidelberg, 2011

    work page 2011

  18. [18]

    Automata theory and model checking

    Orna Kupferman. Automata theory and model checking. In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors,Handbook of Model Checking, pages 107–151. Springer, 2018

    work page 2018

  19. [19]

    Larsen, Christian Schilling, and Jirí Srba

    Kim G. Larsen, Christian Schilling, and Jirí Srba. Simulation relations and applica- tions in formal methods. In Jean-François Raskin, Krishnendu Chatterjee, Laurent Doyen, and Rupak Majumdar, editors,Principles of Systems Design - Essays Dedi- cated to Thomas A. Henzinger on the Occasion of His 60th Birthday, volume 13660 ofLecture Notes in Computer Scie...

    work page 2022

  20. [20]

    Stabilization of networked control sys- tems with weakly hard real-time dropout description

    Steffen Linsenmayer and Frank Allgöwer. Stabilization of networked control sys- tems with weakly hard real-time dropout description. InIEEE Annual Conference on Decision and Control, pages 4765–4770. IEEE, 2017

    work page 2017

  21. [21]

    Control- system stability under consecutive deadline misses constraints

    MartinaMaggio,ArneHamann,EckartMayer-John,andDirkZiegenbein. Control- system stability under consecutive deadline misses constraints. InEuromicro Con- ference on Real-Time Systems, volume 165 ofLIPIcs, pages 21:1–21:24. Schloss Dagstuhl–Leibniz-Zentrum für Informatik, 2020. Over-approximation of weakly-hard constraints 21

    work page 2020

  22. [22]

    Meyer.Matrix Analysis and Applied Linear Algebra

    Carl D. Meyer.Matrix Analysis and Applied Linear Algebra. Society for Industrial and Applied Mathematics, Philadelphia, PA, USA, 2000

    work page 2000

  23. [23]

    Concurrency and automata on infinite sequences.Theory of Com- putation Report, 104(35), 1981

    David Park. Concurrency and automata on infinite sequences.Theory of Com- putation Report, 104(35), 1981. Department of Computer Science, University of Warwick

    work page 1981

  24. [24]

    Be- yond the weakly hard model: Measuring the performance cost of deadline misses

    Paolo Pazzaglia, Luigi Pannocchi, Alessandro Biondi, and Marco Di Natale. Be- yond the weakly hard model: Measuring the performance cost of deadline misses. In30th Euromicro Conference on Real-Time Systems, volume 106 ofLeibniz Inter- national Proceedings in Informatics, pages 10:1–10:22, Dagstuhl, Germany, 2018. Schloss Dagstuhl – Leibniz-Zentrum für Informatik

    work page 2018

  25. [25]

    Springer Spektrum, Berlin, Heidelberg, Germany, 2013

    Wolf Barth Peter Knabner.Lineare Algebra - Grundlagen und Anwendungen. Springer Spektrum, Berlin, Heidelberg, Germany, 2013

    work page 2013

  26. [26]

    Dullerud, and Raphaël M

    Matthew Philippe, Ray Essick, Geir E. Dullerud, and Raphaël M. Jungers. Stabil- ity of discrete-time switching systems with constrained switching sequences.Au- tomatica, 72:242–250, 2016

    work page 2016

  27. [27]

    A note on the joint spectral radius.Indag

    Gian-Carlo Rota and Gilbert Strang. A note on the joint spectral radius.Indag. Math, 22(4):379–381, 1960

    work page 1960

  28. [28]

    Onℓ2-performance of weakly-hard real-time control systems.European Journal of Control, 80:101056, 2024

    Marc Seidel, Simon Lang, and Frank Allgöwer. Onℓ2-performance of weakly-hard real-time control systems.European Journal of Control, 80:101056, 2024. 2024 European Control Conference Special Issue

    work page 2024

  29. [29]

    Seneta.Non-negative Matrices and Markov Chains, Second Edition

    E. Seneta.Non-negative Matrices and Markov Chains, Second Edition. Springer New York, New York, NY, USA, 2006

    work page 2006

  30. [30]

    Moshe Y. Vardi. Automata-theoretic techniques for temporal reasoning. In Patrick Blackburn, J. F. A. K. van Benthem, and Frank Wolter, editors,Handbook of Modal Logic, volume 3 ofStudies in logic and practical reasoning, pages 971–989. North- Holland, 2007

    work page 2007

  31. [31]

    Stabilityandperformanceanaly- sis of control systems subject to bursts of deadline misses

    NilsVreman,AntonCervin,andMartinaMaggio. Stabilityandperformanceanaly- sis of control systems subject to bursts of deadline misses. InEuromicro Conference on Real-Time Systems, volume 196 ofLIPIcs, pages 15:1–15:23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021

    work page 2021

  32. [32]

    InIEEE 28th Real-Time and Embedded Technology and Applications Symposium, pages 228–240, 2022

    Nils Vreman, Richard Pates, and Martina Maggio.WeaklyHard.jl: Scalable analy- sis of weakly-hard constraints. InIEEE 28th Real-Time and Embedded Technology and Applications Symposium, pages 228–240, 2022

    work page 2022

  33. [33]

    Weaklyhard.jl: Scalable analysis of weakly-hard constraints

    Nils Vreman, Richard Pates, and Martina Maggio. Weaklyhard.jl: Scalable analysis of weakly-hard constraints. InIEEE Real-Time and Embedded Technology and Applications Symposium, pages 228–240. IEEE, 2022

    work page 2022

  34. [34]

    Stability of linear systems under extended weakly-hard constraints.IEEE Control Systems Letters, 6:2900–2905, 2022

    Nils Vreman, Paolo Pazzaglia, Victor Magron, Jie Wang, and Martina Maggio. Stability of linear systems under extended weakly-hard constraints.IEEE Control Systems Letters, 6:2900–2905, 2022

    work page 2022

  35. [35]

    Shengjie Xu, Bineet Ghosh, Clara Hobbs, P. S. Thiagarajan, and Samarjit Chakraborty. Safety-aware flexible schedule synthesis for cyber-physical systems using weakly-hard constraints. InProceedings of the 28th Asia and South Pa- cific Design Automation Conference, ASPDAC, pages 46–51, New York, NY, USA,

    work page

  36. [36]

    A The structure ofT m,k,c Proof of Theorem 3.4 Proof.First, we show that the function is well-defined

    Association for Computing Machinery. A The structure ofT m,k,c Proof of Theorem 3.4 Proof.First, we show that the function is well-defined. This means that∀vk:1 = v∈V, n(v k:1, m, k)∈U. Given the constraintAnyMiss(m, k)and its minimal 22 Rieke de Maeyer, Holger Hermanns , Martina Maggio automaton (including⋆where states are merged), for eachv k:1 there ex...

    work page

  37. [37]

    Therefore, in both cases, we haveu′ ∈U

    For the other elements, u′ i ≥u ′ j fori < japplies following the same argument as above,u ′ i =u i−1 and u∈U. Therefore, in both cases, we haveu′ ∈U. Over-approximation of weakly-hard constraints 23 Proof of Theorem 3.7 Proof.We show that there exists a bijective functionf:V→Usuch that (i)f(v init) =u init (ii)∀v, v ′ ∈Vandσ∈Σ: (v, σ, v ′)∈Eif and only i...

    work page