Symbolic Control: Unveiling Free Robustness Margins

Adnane Saoud; Antoine Girard; Youssef Ait Si

REVIEW 4 major objections 5 minor 21 references

Symbolic Control: Unveiling Free Robustness Margins

T0 review · 4 major / 5 minor · reviewed 2026-08-06 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read The paper proves that every symbolic abstraction carries a built-in robustness margin, so the same finite model remains a valid contract for any perturbed system whose disturbance stays below that margin.

desk verdict A well-motivated robustness margin for symbolic abstractions; sufficiency is solid, but the tightness proof has a gap that needs a fix before publication. read the letter →

arxiv 2507.12339 v1 pith:J7ESYAH2 submitted 2025-07-16 eess.SY cs.SY

Youssef Ait Si , Antoine Girard , Adnane Saoud This is my paper · ORCID

classification eess.SYcs.SY

keywords robustcontrolsymbolicrobustnessmarginalternatingsimulationrelationreachabilityanalysisabstraction-basedcontrollersynthesisperturbeddiscrete-timesystemstemporallogicspecifications

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

Given a discrete-time control system and a finite symbolic abstraction built from reachable-set over-approximations, the paper proves that the abstraction is not only a model of the disturbance-free system: it is also a valid model of every perturbed version whose additive disturbance, at each state and input, is smaller than a margin that can be read off from the abstraction's geometry. The margin is strictly positive everywhere, so this robustness is free -- it comes from the slack between the over-approximated reachable set and the boundary of the set of symbolic successors. The paper gives a constructive formula for the margin, a uniform version valid for all states and inputs, and a tightness result: when reachable sets are computed exactly, any disturbance larger than the margin breaks the behavioral relation, and with a $\delta$-over-approximation the breaking threshold is the margin plus $\delta$. It then shows how a controller synthesized for the disturbance-free abstraction refines to the perturbed system, and how to choose among admissible inputs the one maximizing the margin.

What carries the argument

The load-bearing object is the robustness-margin map $\eta(q,v,A)$, defined as the supremum radius by which the over-approximated reachable set $\mathrm{cl}(\bar f(q,v,D))$ can be inflated while remaining inside the interior of $Q^{-1}(A)$, the union of cells that are symbolic successors. Lemma 3.1 shows this radius is always positive: because a symbolic transition exists exactly when the over-approximated reachable set touches the closure of the successor cell, the set must actually lie strictly inside the interior of the union of successors. Theorem 3.2 converts that geometric slack into an admissible disturbance level, and the $\delta$-over-approximation gap into the tightness error. The same slack appears as the uniform margin $\min_{q,v}\eta(q,v,\Delta_d(q,v))$ in Corollary 3.3.

What would settle it

Pick a cell $q$ and input $u$ in the paper's double-integrator example (exact reachable sets, $\delta=0$, uniform margin $0.01125$), locate a point $z\in q$ at which the local margin attains its minimum, and apply a constant disturbance of magnitude $\varepsilon(z,u)+0.001$. If the one-step successor never leaves the union of symbolic successor cells, the tightness assertion of Theorem 3.2 is false; if it lands outside, tightness is confirmed on that instance.

Watch

Extended reading notes

Core claim

Let $S_d(\Sigma)$ be the symbolic model whose transitions come from an over-approximation $\bar f$ of the reachable set, and let $\eta(q,v,A)$ be the largest radius $\varepsilon$ such that the inflated reachable set $\mathrm{cl}(\bar f(q,v,D)) + \mathcal{B}_{\varepsilon}(0)$ stays inside the interior of $Q^{-1}(A)$. The paper's central claim is that the relation $\{(x,q): x\in q\}$ is an alternating simulation relation from $S_d(\Sigma)$ to the perturbed system $S(\Sigma_\mu)$ whenever $\mu(x,u) < \eta(Q(x),u,\Delta_d(Q(x),u))$ for all state-input pairs. Conversely, when $\bar f$ is a $\delta$-over-approximation with closed values, if $\mu(x,u) > \eta(Q(x),u,\Delta_d(Q(x),u)) + \delta$ for some pair, the relation is not an alternating simulation relation. The margin is therefore both a certificate of robustness and, up to the over-approximation error $\delta$, the largest disturbance the abstraction can tolerate; with exact reachable sets the margin is tight.

Load-bearing premise

The tightness half of the main theorem relies on the assumption that the over-approximated reachable set is closed and bounded enough for the worst-case point inside a cell to exist; if that assumption fails, the sufficiency direction still holds but the claim that exceeding the margin destroys the simulation relation is not established.

Editorial extensions

If this is right

Any controller synthesized on the disturbance-free symbolic model remains correct for the perturbed system under the same specification, provided $\mu(x,u)<\varepsilon(x,u)$ at every step.
The uniform margin $\varepsilon = \min_{q,v}\eta(q,v,\Delta_d(q,v))$ is strictly positive and protects all states and inputs simultaneously, so no per-state disturbance measurement is needed.
If reachable sets are computed exactly, the margin is tight: adding any disturbance above the margin destroys the alternating simulation relation.
With a $\delta$-over-approximation of reachable sets, the threshold shifts by $\delta$, so improving reachability tightness directly enlarges the guaranteed robustness.
Finer discretization of the state and input spaces reduces the uniform margin, making the known trade-off between abstraction accuracy and disturbance tolerance explicit.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

The margin could be monitored online: compare the current disturbance estimate against $\varepsilon(x,u)$ and recompute the abstraction only when the margin is violated, rather than over-approximating disturbances a priori.
Because the uniform margin is a minimum over finitely many cells, it will often be dominated by the tightest transition; the same machinery could be applied locally, cell by cell, to avoid wasting reachability effort on transitions with large slack.
The geometric argument is not tied to alternating simulation specifically -- analogous slack in any abstraction relation (for instance feedback refinement or approximate simulation) should yield a similar free disturbance margin.
A specification-aware version that computes the margin for the predecessor operator rather than the full successor set would likely give larger effective margins for safety and reachability tasks.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

Dear colleague,

The paper is worth your time if you work on abstraction-based control: it makes explicit a robustness margin that is implicit in every symbolic abstraction. The sufficiency result (Theorem 3.2, item 2) is correct and clean: if the additive disturbance μ(x,u) is pointwise below η(Q(x),u,Δ_d(Q(x),u)), the relation {(x,q): x∈q} remains an alternating simulation from the abstraction to the perturbed system. That gives a direct way to reuse a disturbance-free abstraction and controller for a whole family of perturbed systems. The uniform-margin corollary and the controller-refinement proposition are straightforward and useful. The observation that tightness of the margin tracks the tightness of the reachable-set over-approximation is also correct in spirit.

The weak point is the tightness half (Theorem 3.2, item 3). The proof needs a z∈q that witnesses the margin in the sense of Eq. (8): a single point whose expanded reachable fiber leaves the target for every ε above the local margin. But η is defined as a supremum over the whole cell's over-approximated reachable set. The supremum yields a point of that cell-level set, not a point belonging to the fiber of a specific z. Extracting such a z requires compactness of \bar f(q,u,D) and some upper hemicontinuity of x↦\bar f(x,u,D), or an explicit infimum-over-x definition of the margin. The paper assumes only that \bar f(q,u,D) is closed, which is not enough. The sufficiency direction does not depend on this step, and the example in Fig. 4 shows the expected behavior, but the formal tightness claim, and the δ=0 'tightness' remark, are not established by the proof as written.

The examples are purely illustrative; no code or data is shipped, so the practical gain is asserted rather than demonstrated. The notation in the δ-overapproximation part of the proof is also under-specified, which makes the tightness argument harder to check.

On novelty: the sufficiency half is close to what some of us would call folklore, but the state/input-dependent margin and the explicit tightness analysis are a real extension of [11]. The paper is honest about its limitations and the literature is cited appropriately.

Who should read it: people working on symbolic controller synthesis who need robustness guarantees. The paper deserves a serious referee, but the tightness proof needs a missing hypothesis or a redefinition of η before publication. I would send it to review with a request for revision, not desk-reject it. I would bring it to a reading group, and I would cite it — but only the sufficiency half until the gap is closed.

Referee Report

4 major / 5 minor

Summary. The paper proposes a notion of robustness margin for symbolic models of discrete-time control systems. Given an abstraction S_d(Σ) of a disturbance-free system, it defines a state- and input-dependent quantity η from the over-approximated reachable set and the successor cells, and proves (Theorem 3.2) that if an additive disturbance μ is pointwise below this margin, the same alternating simulation relation still holds between the abstraction and the perturbed system; it further claims a tightness result up to the reachability error δ, derives a uniform margin (Corollary 3.3), and applies the margin to controller refinement (Proposition 3.4). Two examples illustrate the computation and use of the margins.

Significance. The conceptual contribution is attractive: if the main theorem is correct, a precomputed symbolic model carries a quantitative guarantee on how much disturbance it can tolerate, and controllers synthesized for the disturbance-free abstraction can be reused for all perturbed systems below the margin. The sufficiency direction of Theorem 3.2 and the controller-refinement proposition are clean and appear sound; the paper also gives concrete algorithmic recipes and two worked examples, which help communicate the idea. However, the advertised tightness results depend on several hypotheses that are either missing or not stated precisely: without them, the negative half of Theorem 3.2 and the uniform-margin corollary are not established. I regard the paper as a promising contribution whose central claims need a substantial proof repair rather than a rejection.

major comments (4)

[Section 3.1, proof of Theorem 3.2, first item] The proof infers from cl(\bar f(q,u,D)) ⊆ Int(Q^{-1}(Δ_d(q,u))) that there exists α>0 with cl(\bar f(q,u,D))+B_α(0) ⊆ Int(Q^{-1}(Δ_d(q,u))). This inference is not valid without compactness of cl(\bar f(q,u,D)) or a positive-distance condition: a closed noncompact set can lie inside an open set while having distance zero to its complement (for example, a graph approaching the boundary at infinity). The paper does not assume X bounded or \bar f(q,u,D) compact, so the claimed ε(x,u)>0, and the positivity part of Corollary 3.3, are not established as stated. Adding an assumption that cl(\bar f(q,u,D)) is compact, or defining the margin with an explicit positive-distance condition, would repair this step.
[Section 3.1, Theorem 3.2, item 3, Eq. (8)] The existence of a single z∈q satisfying Eq. (8) for every ε0>ε(z,u) is asserted without proof. The margin η(q,u,A) in Eq. (3) is a supremum taken over the cell-level over-approximated reachable set \bar f(q,u,D); it does not by itself provide a point z whose pointwise reachable set attains that supremum. Extracting such a z requires compactness of cl(\bar f(q,u,D)) and upper hemicontinuity of x↦\bar f(x,u,D), or an explicit infimum-over-x definition of the margin, none of which is stated. Absent this, the tightness claim in item 3, and the analogous claim in Eq. (11) of Corollary 3.3, are not established; the sufficiency half of the theorem is unaffected.
[Section 3.1, proof of Theorem 3.2, third item] The proof uses the equality cl(\bar f(z,u,D)) = \bar f(z,u,D) after selecting z∈q. The closedness hypothesis in the theorem concerns cell-level sets \bar f(q,v,D) for q∈X_d, v∈U_d, not the pointwise sets \bar f(z,u,D) for continuous states z. Unless \bar f(q,v,D) is defined as the union of pointwise images and pointwise closedness is assumed, this equality is unjustified. The same issue appears in Corollary 3.3.
[Section 3.1, footnote 1 and proof of the third item] The δ-overapproximation condition should be stated with a clear inclusion direction. As printed, footnote 1 appears to read f(x,u,D) ⊆ \bar f(x,u,D)+B_δ(0), whereas the proof needs the opposite inclusion, \bar f(z,u,D) ⊆ f(z,u,D)+B_δ(0), to justify \bar f(z,u,D)+B_{μ-δ}(0) ⊆ f(z,u,D)+B_μ(0). If the intended definition is \bar f(x,u,D) ⊆ f(x,u,D)+B_δ(0), it should be stated explicitly and the term 'overapproximation' clarified, since many standard reachable-set overapproximations are only guaranteed to satisfy the forward inclusion f ⊆ \bar f+B_δ unless a two-sided error bound is imposed.

minor comments (5)

[Section 3.1, proof of Theorem 3.2] The sentence 'To show that R in (10) is not an alternating simulation relation' should refer to Eq. (5), not Eq. (10), which belongs to Corollary 3.3.
[Section 3.4, Eq. (13)] The Argmax operation in Eq. (13) returns a set, so the expression defines a set-valued map rather than a deterministic controller; a tie-breaking rule or a choice function should be specified.
[Throughout] The overline distinguishing \bar f from f is frequently lost in the typeset equations, which makes the direction of the δ-overapproximation assumption difficult to verify; using a distinct symbol for the overapproximated reachable map would improve readability.
[Throughout] There are several typos: 'there exits' should be 'there exists' in the proof of Theorem 3.2, '𝑞∈𝑋𝑞' should presumably be '𝑞∈𝑋𝑑', and 'Σ̄ 𝜇' in Corollary 3.3 should be 'Σ_𝜇'.
[Section 4.1, Table 1] The row for N_u=3 shows the uniform margin staying constant at 0.0237 for N_x=1600, 3200, and 6400 before dropping at 12800; a brief explanation of this plateau would help the reader interpret the trade-off between discretization and robustness.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the robustness margin is a defined quantity and the simulation property is proved directly from its definition; the tightness witness gap is a mathematical proof gap, not a circular reduction.

full rationale

The paper's main result (Theorem 3.2) is not circular. The margin eta(q,v,A) in Eq. (3) is defined as the supremum of radii epsilon for which the over-approximated reachable set, expanded by B_epsilon(0), remains inside Int(Q^{-1}(A)). The sufficiency direction then proves that any perturbed transition with mu < epsilon lands in that interior, hence in a successor cell; this is a direct consequence of the definition of eta, not a fitted parameter or a hidden assumption of the conclusion. Lemma 3.1, which supplies positivity of eta, follows from the very definition of the symbolic transition relation (closure intersection), so no empirical input is being repackaged as a prediction. Self-citations ([8], [16], [17]) are background material on symbolic control and resilience metrics and are not load-bearing for the main theorems; the abstraction and reachability foundations are standard external results ([1], [13], [18]). The tightness half (Theorem 3.2, item 3) asserts an unproved witness point z in Eq. (8) used to realize the supremum in Eq. (3); this is a genuine mathematical gap requiring compactness or upper hemicontinuity of the over-approximation, but it is not circularity because the argument does not assume the negation of the target relation. No load-bearing self-citation chain or definitional identity between input and output is exhibited. Score 0 reflects the absence of circular steps; the proof gap should be addressed as a correctness issue.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

The main theorems introduce no fitted constants; η and ε are computed from the abstraction and reachable-set geometry. The numerical examples use hand-chosen discretization sizes, sampling period, disturbance bounds, and target regions, but these do not enter the central claim. No new physical entities are postulated.

assumptions (4)

domain assumption The state space X is bounded and the closed over-approximated reachable sets \bar f(q,u,D) are compact.
Needed for the margin ε(x,u) to be positive and for the tightness witness z to exist; the paper only states closedness.
domain assumption The over-approximation \bar f satisfies the tightness inclusion \bar f(q,u,D) ⊆ f(q,u,D)+B_δ(0) in addition to being an outer approximation.
Used in the proof of Theorem 3.2 item 3 to replace \bar f+B_{μ−δ} by a subset of f+B_μ; the footnote's notation is ambiguous.
domain assumption The alternating simulation framework and finite abstraction construction from [18] are valid for the considered systems.
The paper relies on this background to assert that S_d(Σ) ≼ S(Σ) exists for the disturbance-free system.
domain assumption Each point of X belongs to exactly one cell of the finite partition, so the quantizer Q is a total function.
The relation (x,q) iff x∈q requires a total quantizer; boundary convention is not specified.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Symbolic Control: Unveiling Free Robustness Margins." pith.science (2026). https://pith.science/paper/J7ESYAH2

@misc{pith2026250712339,
  author       = {Pith},
  title        = {Pith review of: Symbolic Control: Unveiling Free Robustness Margins},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/J7ESYAH2}},
  note         = {Machine review of arXiv:2507.12339}
}

read the original abstract

This paper addresses the challenge of ensuring robustness in the presence of system perturbations for symbolic control techniques. Given a discrete-time control system that is related to its symbolic model by an alternating simulation relation. In this paper, we focus on computing the maximum robustness margin under which the symbolic model remains valid for a perturbed-version of the discrete-time control system. We first show that symbolic models are inherently equipped with a certain free robustness margins. We then provide constructive procedures to compute uniform and non-uniform (state and input dependent) robustness margins. We also show that the tightness of the robustness margin depends on the tightness of the reachability technique used to compute the symbolic model. We then explain how the computed robustness margin can be used for the sake of controller synthesis. Finally, we present two illustrative examples to demonstrate the effectiveness of our approach.

Figures

Figures reproduced from arXiv: 2507.12339 by the authors.

**Figure 1.** The first figure displays the overapproximation of the reachable set for the discrete state 𝑞1 under the discrete input 𝑢1 . It also illustrates the margin 𝜂(𝑞1 , 𝑢1 , Δ𝑑 (𝑞1 , 𝑢1 )) = 𝜀1 that can be added to the borders of this overapproximation while preserving the same set of successors. The second figure shows the equivalent automata for the transitions from the discrete state 𝑞1 under the discrete input 𝑢1 . Co… view at source ↗

**Figure 2.** The maximal admissible robustness margin for each state [PITH_FULL_IMAGE:figures/full_fig_p007_2.png] view at source ↗

**Figure 3.** The input value maximizing the robustness margin for each state. discrete-time dynamics of the system are defined by the following equations: ⎧ ⎪ ⎨ ⎪ ⎩ 𝑥 1 𝑘+1 = 𝑥 1 𝑘 + 𝜏 ( 𝑢 1 𝑘 cos ( 𝑥 3 𝑘 ) + 𝑤1 𝑘 ) 𝑥 2 𝑘+1 = 𝑥 2 𝑘 + 𝜏 ( 𝑢 1 𝑘 sin ( 𝑥 3 𝑘 ) + 𝑤2 𝑘 ) 𝑥 3 𝑘+1 = 𝑥 3 𝑘 + 𝜏 ( 𝑢 2 𝑘 + 𝑤3 𝑘 ) (mod2𝜋) where (𝑢 1 , 𝑢2 ) ∈ [0.25, 1] × [−1, 1] are the control inputs of the system representing the robot’s linear and angular… view at source ↗

Figures from the paper (1 more)

**Figure 5.** Figure 5: Simulation of three trajectories of robot dynamic with and without perturbation starting from two initial states 𝑥0 = (0.5, 4) and 𝑥1 = (0.5, 5). 5. Conclusion We have introduced a new concept of maximal robustness margin for discrete-time dynamical systems. This quan…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

21 extracted references · 18 canonical work pages

[11]

Nonlinear Analysis: Hybrid Systems 22, 1–15

Liu,J.,Ozay,N.,2016.Finiteabstractionswithrobustnessmarginsfor temporal logic-based control synthesis. Nonlinear Analysis: Hybrid Systems 22, 1–15

work page 2016
[1]

Setpropagationtechniques for reachability analysis

Althoff,M.,Frehse,G.,Girard,A.,2021. Setpropagationtechniques for reachability analysis. Annual Review of Control, Robotics, and Autonomous Systems 4, 369–395

work page 2021
[2]

Alter- nating refinement relations, in: Sangiorgi, D., de Simone, R

Alur, R., Henzinger, T.A., Kupferman, O., Vardi, M.Y., 1998. Alter- nating refinement relations, in: Sangiorgi, D., de Simone, R. (Eds.), CONCUR ’98: Concurrency Theory, 9th International Conference, Nice, France, September 8-11, 1998, Proceedings, Springer. pp. 163–178. URL: https://doi.org/10.1007/BFb0055622, doi:10.1007/ BFB0055622

doi:10.1007/bfb0055622 1998
[3]

Synthesis of input-to-state attractivitycontrollersfortransitionsystemswithdisturbances

Apaza-Perez, W.A., Girard, A., 2024. Synthesis of input-to-state attractivitycontrollersfortransitionsystemswithdisturbances. IEEE Transactions on Automatic Control

work page 2024
[4]

Bai,Y.,Mallik,K.,2020. Accurateabstractionsforcontrollersynthe- siswithnon-uniformdisturbances,in:FormalMethodsandSoftware Engineering: 22nd International Conference on Formal Engineering Methods, ICFEM 2020, Singapore, Singapore, March 1–3, 2021, Proceedings 22, Springer. pp. 297–307

work page 2020
[5]

Bai, Y., Mallik, K., Schmuck, A.K., Zufferey, D., Majumdar, R.,

work page
[6]

volume 89

Belta,C.,Yordanov,B.,Gol,E.A.,2017.Formalmethodsfordiscrete- time dynamical systems. volume 89. Springer

work page 2017
[7]

Resilience to intermittent assumption violations in reactive synthesis, in: Proceedings of the 17th interna- tional conference on Hybrid systems: computation and control, pp

Ehlers, R., Topcu, U., 2014. Resilience to intermittent assumption violations in reactive synthesis, in: Proceedings of the 17th interna- tional conference on Hybrid systems: computation and control, pp. 203–212

work page 2014

Show all 21 references

[8]

Techniques de l’Ingénieur

Girard,A.,Meyer,P.J.,Saoud,A.,2024.Approchessymboliquespour le contrôle des systèmes non linéaires. Techniques de l’Ingénieur

2024
[9]

Multi-layered abstraction-based controller synthesis for continuous-time systems, in: Prandini, M., Deshmukh, J.V

Hsu,K.,Majumdar,R.,Mallik,K.,Schmuck,A.,2018. Multi-layered abstraction-based controller synthesis for continuous-time systems, in: Prandini, M., Deshmukh, J.V. (Eds.), Proceedings of the 21st In- ternationalConferenceonHybridSystems:ComputationandControl (partofCPSWeek),HSCC2...

2018
[10]

Reachability analysis of linear systemsusingsupportfunctions.NonlinearAnalysis:HybridSystems 4, 250–262

Le Guernic, C., Girard, A., 2010. Reachability analysis of linear systemsusingsupportfunctions.NonlinearAnalysis:HybridSystems 4, 250–262

2010
[12]

Augmented finite transition sys- tems as abstractions for control synthesis

Nilsson, P., Ozay, N., Liu, J., 2017. Augmented finite transition sys- tems as abstractions for control synthesis. Discret. Event Dyn. Syst. 27, 301–340. URL: https://doi.org/10.1007/s10626-017-0243-z, doi:10.1007/S10626-017-0243-Z

2017 doi
[13]

Feedback refinement relationsforthesynthesisofsymboliccontrollers

Reissig, G., Weber, A., Rungger, M., 2017. Feedback refinement relationsforthesynthesisofsymboliccontrollers. IEEETransactions on Automatic Control 62, 1781–1796

2017
[14]

A notion of robustness for cyber- physicalsystems

Rungger, M., Tabuada, P., 2015. A notion of robustness for cyber- physicalsystems. IEEETransactionsonAutomaticControl61,2108– 2123

2015
[15]

Accurate reachability analysis of uncertainnonlinearsystems,in:Proceedingsofthe21stinternational conferenceonhybridsystems:Computationandcontrol(partofCPS week), pp

Rungger, M., Zamani, M., 2018. Accurate reachability analysis of uncertainnonlinearsystems,in:Proceedingsofthe21stinternational conferenceonhybridsystems:Computationandcontrol(partofCPS week), pp. 61–70

2018
[16]

Compositional and efficient controller synthesis for cyber-physical systems

Saoud, A., 2019. Compositional and efficient controller synthesis for cyber-physical systems. Ph.D. thesis. Université Paris Saclay (COmUE)

2019
[17]

Temporal logic resilience for dynamical systems

Saoud, A., Jagtap, P., Soudjani, S., 2024. Temporal logic resilience for dynamical systems. CoRR abs/2404.19223. URL: https:// Y.A Si et al.:Preprint submitted to Elsevier Page 8 of 9 Unveiling Free Robustness Margins doi.org/10.48550/arXiv.2404.19223, doi: 10.48550/ARXIV.2404...

2024 doi arXiv
[18]

Verification and control of hybrid systems: a symbolic approach

Tabuada, P., 2009. Verification and control of hybrid systems: a symbolic approach. Springer Science and Business Media

2009
[19]

To- wards robustness for cyber-physical systems

Tabuada, P., Caliskan, S.Y., Rungger, M., Majumdar, R., 2014. To- wards robustness for cyber-physical systems. IEEE Transactions on Automatic Control 59, 3151–3163

2014
[20]

Symbolicmodels for nonlinear control systems without stability assumptions

Zamani,M.,Pola,G.,Mazo,M.,Tabuada,P.,2011. Symbolicmodels for nonlinear control systems without stability assumptions. IEEE Transactions on Automatic Control 57, 1804–1809. Y.A Si et al.:Preprint submitted to Elsevier Page 9 of 9

2011
[2019]

Incremental abstraction computation for symbolic controller synthesisinachangingenvironment,in:2019IEEE58thConference on Decision and Control (CDC), IEEE. pp. 6261–6268

Pith tools

Reviewed August 6, 2026 · model on record in the stance chip above.

[1] [11]

Nonlinear Analysis: Hybrid Systems 22, 1–15

Liu,J.,Ozay,N.,2016.Finiteabstractionswithrobustnessmarginsfor temporal logic-based control synthesis. Nonlinear Analysis: Hybrid Systems 22, 1–15

work page 2016

[2] [1]

Setpropagationtechniques for reachability analysis

Althoff,M.,Frehse,G.,Girard,A.,2021. Setpropagationtechniques for reachability analysis. Annual Review of Control, Robotics, and Autonomous Systems 4, 369–395

work page 2021

[3] [2]

Alter- nating refinement relations, in: Sangiorgi, D., de Simone, R

Alur, R., Henzinger, T.A., Kupferman, O., Vardi, M.Y., 1998. Alter- nating refinement relations, in: Sangiorgi, D., de Simone, R. (Eds.), CONCUR ’98: Concurrency Theory, 9th International Conference, Nice, France, September 8-11, 1998, Proceedings, Springer. pp. 163–178. URL: https://doi.org/10.1007/BFb0055622, doi:10.1007/ BFB0055622

doi:10.1007/bfb0055622 1998

[4] [3]

Synthesis of input-to-state attractivitycontrollersfortransitionsystemswithdisturbances

Apaza-Perez, W.A., Girard, A., 2024. Synthesis of input-to-state attractivitycontrollersfortransitionsystemswithdisturbances. IEEE Transactions on Automatic Control

work page 2024

[5] [4]

Bai,Y.,Mallik,K.,2020. Accurateabstractionsforcontrollersynthe- siswithnon-uniformdisturbances,in:FormalMethodsandSoftware Engineering: 22nd International Conference on Formal Engineering Methods, ICFEM 2020, Singapore, Singapore, March 1–3, 2021, Proceedings 22, Springer. pp. 297–307

work page 2020

[6] [5]

Bai, Y., Mallik, K., Schmuck, A.K., Zufferey, D., Majumdar, R.,

work page

[7] [6]

volume 89

Belta,C.,Yordanov,B.,Gol,E.A.,2017.Formalmethodsfordiscrete- time dynamical systems. volume 89. Springer

work page 2017

[8] [7]

Resilience to intermittent assumption violations in reactive synthesis, in: Proceedings of the 17th interna- tional conference on Hybrid systems: computation and control, pp

Ehlers, R., Topcu, U., 2014. Resilience to intermittent assumption violations in reactive synthesis, in: Proceedings of the 17th interna- tional conference on Hybrid systems: computation and control, pp. 203–212

work page 2014