Complete Abstractions of Monotone Control Systems: From Model-based to Data-Driven Systems

Adnane Saoud; Anas Makdesi; Antoine Girard; Mohamed Maghenem; Murat Arcak

REVIEW 2 major objections 5 minor 40 references

Complete Abstractions of Monotone Control Systems: From Model-based to Data-Driven Systems

T0 review · 2 major / 5 minor · reviewed 2026-08-10 · deepseek-v4-flash

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

Pith's one-line read For a monotone control system, a pair of coarse models can bracket the exact controllability of the original system.

desk verdict Model-based complete abstractions are solid and new; the data-driven theorems need an additional monotone-partition hypothesis before they are true as stated. read the letter →

arxiv 2608.06689 v1 pith:4D7I6VAN submitted 2026-08-07 eess.SY cs.SY

Adnane Saoud , Anas Makdesi , Mohamed Maghenem , Antoine Girard , Murat Arcak This is my paper · ORCID

classification eess.SYcs.SY MSC 93C5568Q6093C65

keywords monotonecontrolsystemsalternatingsimulationsymboliccompleteabstractionsdata-drivenabstractionformalverificationtransitionsafetysynthesis

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

This paper introduces a behavioral relation called approximate strong upper alternating simulation (ASUAS), an order-based notion of simulation tailored to monotone control systems. Using it, the authors build two finite abstractions of a discrete-time monotone system, an upper-sparse and a lower-sparse abstraction, and prove that they bracket the original system in the ASUAS order. The practical payoff is two-sided: a controller synthesized for the upper abstraction refines into a controller for the original, and if no controller exists for the lower abstraction, then no controller exists for the original. The same bracketing is rederived when the abstractions are built directly from finite sampled data rather than from the model. A tunable discretization parameter provably controls the conservativeness gap between the two abstractions, so the method yields a complete abstraction pair for this class of systems.

What carries the argument

The central object is the $\varepsilon$-approximate strong upper alternating simulation (ASUAS), a relation $R$ between concrete and abstract states requiring $H_1(x_1) \leq H_2(x_2)+\varepsilon$ and, for every abstract input $u_2$, enabling every concrete input $u_1 \leq u_2$ with matching successors. This order-only condition, instead of distance-based closeness, is what makes monotone systems amenable to exact bracketing. The upper-sparse abstraction keeps the upper corners $x_2^q$ of each cell and transitions via $f(x_2^q,u,d_2^m)$ (the maximum disturbance); the lower-sparse abstraction keeps lower corners $x_1^q$ and transitions via $f(x_1^q,u,d_2^m)$. Monotonicity ensures these two extreme transitions dominate every concrete transition from the cell, yielding the two ASUAS inequalities. The conservativeness results rest on Lemma 1, which uses the derivative bounds $0 \leq \partial f_i/\partial x_j \leq \alpha_{ij}$ to show that a cell of width $\eta$ can be compensated by a perturbation $\varepsilon = \alpha\eta$.

What would settle it

Run the data-driven construction on a monotone system using a non-monotone partition, for example two adjacent cells with ordered upper corners but crossed lower corners as in the third partition of Figure 3, and check whether $U_{\Sigma_D} \preceq^0_u U_\Sigma$ still holds; a single transition where the data-driven successor jumps above or below the model-based successor would refute Theorem 4 as stated.

Watch

Extended reading notes

Core claim

For a discrete-time monotone control system whose state space is lower closed, the upper-sparse abstraction $U_\Sigma$ and lower-sparse abstraction $L_\Sigma$ built from the same partition satisfy $U_\Sigma \preceq^0_u S_\Sigma \preceq^0_u L_\Sigma$. Consequently, controller synthesis for $U_\Sigma$ is sound (any abstract controller refines to the concrete system) and the absence of a controller for $L_\Sigma$ is a certificate of impossibility for the concrete system. When data points are sampled under the maximum disturbance, data-driven versions $U_{\Sigma_D}$ and $L_{\Sigma_D}$ satisfy $U_{\Sigma_D} \preceq^0_u U_\Sigma \preceq^0_u S_\Sigma \preceq^0_u L_\Sigma \preceq^0_u L_{\Sigma_D}$, giving the same two-sided guarantee without an explicit model. Theorems 3 and 5 give explicit inequalities, $\varepsilon_i \geq \sum_j \alpha_{ij}\eta_j$, that translate a desired precision into a required discretization parameter in both the model-based and data-driven settings.

Load-bearing premise

The data-driven guarantees hold only when the partition respects the partial order (cells' upper bounds are ordered whenever the cells are ordered); a non-monotone partition can break the bracketing even when all other assumptions hold.

Editorial extensions

If this is right

Safety controllers synthesized on the upper-sparse abstraction can be refined to the original monotone system without loss of correctness.
If the lower-sparse abstraction admits no controller for a lower-closed specification, the original system admits none, so controller-synthesis tools can now give negative answers with certainty.
The conservativeness gap between the two abstractions shrinks to any prescribed precision $\varepsilon$ by refining the grid according to $\varepsilon_i \geq \sum_j \alpha_{ij}\eta_j$.
Data-driven versions built purely from finite samples inherit both guarantees, so no model equations are needed while preserving soundness and completeness.
With uniform random sampling, the same guarantees hold with probability at least $1-\beta$ once the sample count exceeds the bound in Proposition 2.

Reading between the lines

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

The bracketing idea should transfer to mixed-monotone systems, where extremal decompositions replace plain monotone bounds; the ASUAS relation's order-only condition is a natural fit.
The completeness guarantee suggests a practical synthesis workflow: start coarse, attempt upper synthesis, and if it fails refine until either a controller is found or the lower abstraction also fails, with the gap provably shrinking.
For upper-closed specifications, a mirror-image construction swapping the roles of $U_\Sigma$ and $L_\Sigma$ is implied by the paper's remark that analogous results hold, though the details are not worked out.
The probabilistic sample bound could be turned into an adaptive stopping rule: sample until every cell's critical region is hit rather than fixing $N$ in advance, potentially reducing data cost.

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

Plainly: the model-based half of this paper is good and genuinely new; the data-driven half as stated is not fully proven. Theorems 4 and 5 are missing a hypothesis the proofs need.

The new thing here is the complete abstraction pair: an upper-sparse abstraction that is sufficient and a lower-sparse abstraction that is necessary, joined by a new ASUAS relation which replaces output closeness with output ordering. That is a real step beyond the sound-only abstractions for monotone systems, and it gives a practical way to certify controller absence. Theorem 2 is proved cleanly under the stated assumptions. Theorem 3, which tunes the conservativeness gap through the discretization parameter, also checks out. The numerical experiments are honest: they illustrate the bracketing and do not calibrate anything. No circularity; the αij and ξ are user-specified bounds, not fit to results.

The soft spot is in Section V. Theorems 4 and 5 are stated under Assumption 3, but the transition definitions (18) and (21) require a componentwise extremum over all cells intersecting a down-set or up-set, and for an arbitrary rectangular partition that extremum may not be attained by any cell's bound. A partition like [0,2]^2 split into A=[0,1]×[0,2], B=[1,2]×[0,1], C=[1,2]×[1,2] violates Assumption 4, and a down-set can intersect two cells with incomparable upper bounds, leaving the max in (18) undefined. Assumption 4—monotonicity of the partition—is exactly what makes the cell containing the extremal data point dominate all intersecting cells, and the proofs of Theorems 4 and 5 use that implicitly when they assert x^{q'_1}_1 ≤ x^{q'_2}_1. Section V never states Assumption 4. This is repairable: add Assumption 4 to the hypotheses and reference it explicitly in the proofs. There is also a minor wording issue: the paper promises unicity of the successor in (18), but unless the partition is monotone there is not even existence, and even with Assumption 4 you get determinism only after choosing the extremal cell, not uniqueness of the cell itself.

The model-based core holds up, so this deserves a serious referee. The right outcome is conditional: accept after fixing the data-driven assumptions. The paper will be useful to symbolic control and monotone systems people, and the complete abstraction pair is worth citing even before the data-driven half is patched.

Referee Report

2 major / 5 minor

Summary. The paper introduces a new behavioral relation, approximate strong upper alternating simulation (ASUAS), which replaces the usual output-closeness condition with an output-ordering condition. Building on ASUAS, the authors construct upper- and lower-sparse abstractions UΣ and LΣ for discrete-time monotone control systems and prove the bracketing UΣ ≼^0_u SΣ ≼^0_u LΣ, so that a controller for UΣ refines to SΣ and absence of a controller for LΣ certifies absence for SΣ. Theorem 3 shows that the gap between the two abstractions can be controlled by the space-discretization parameter η through the Jacobian bound ε_i ≥ ∑_j α_ij η_j. Section V extends the construction to a data-driven setting, where abstractions UΣD, LΣD are built from a finite dataset of transitions sampled under the maximum disturbance; Theorem 4 claims UΣD ≼^0_u UΣ ≼^0_u SΣ ≼^0_u LΣ ≼^0_u LΣD, and Theorem 5 adds a conservativeness bound with a probabilistic version in Proposition 2. The theoretical results are illustrated on an adaptive cruise control example.

Significance. If the claims hold, the paper makes a significant contribution to symbolic control: it provides the first complete abstraction pair for monotone systems that does not require incremental stability, and it does so with a constructive way to tune the abstraction gap. The model-based part (Theorems 2 and 3) appears sound, and the proofs are genuinely theorem-based: the Jacobian bounds αij and the sampling interval ξ are user-provided, not fitted to the numerical results. The data-driven extension addresses a practically important problem, and the PAC-style sample bound in Proposition 2 is supported by a Monte Carlo validation. The main flaw is that the data-driven Theorems 4 and 5 miss a necessary monotone-partition hypothesis in their statements, which makes this half of the paper incomplete as written. The issue is repairable without changing the overall approach.

major comments (2)

[Section V, Theorems 4 and 5, Eqs. (18) and (21)] The data-driven theorems are stated under Assumption 3 only, but their proofs require the monotone-partition property of Assumption 4. The transition definitions (18) and (21) require that the sets of upper bounds, respectively lower bounds, of cells intersecting the down-set Qu(q,u) and the up-set Ql(q,u) have a componentwise maximum, respectively minimum, that is attained by one of the intersecting cells. Assumption 3 does not guarantee this. For example, with X=[0,2]^2 partitioned into A=[0,1]×[0,2], B=[1,2]×[0,1], C=[1,2]×[1,2], and Qu=↓(1.5,0.5), the cells A and B intersect Qu and have upper bounds (1,2) and (2,1), whose componentwise maximum (2,2) is not the upper bound of any cell intersecting Qu, so (18) has no solution. Assumption 4(i)-(ii) is exactly the condition that makes such extrema well-defined and validates the proof steps that compare x^{q'_1}_1 with x^{q'_2}_1 and x^{q'_1}_2 with x^{q'_2}_2. I recommend adding Assumption 4 to the hypotheses of Theorems 4 and 5 and to the definitions of UΣD and LΣD, and explicitly invoking it in the proofs.
[Section IV-B, proof of Theorem 3, Eq. (14)] The proof states that for u2 ∈ U_a^L(q2), the point max{f(x^{q2}_1,u2,d^m_2)+Ωε(0)} belongs to X. This is not generally true: since X is only lower closed, the ε-ball around a point of X can extend outside X in the upward direction. The subsequent inclusion ↓max{...} ⊆ ↓X ⊆ X may therefore fail. The conclusion that u1 ∈ U_a^U(q1) can be obtained more directly, because the transition relation of the upper-sparse abstraction only needs the point f(x^{q1}_2,u1,d^m_2) to lie in X, which follows from f mapping X into X and the partition covering X. The proof should be revised to avoid the unproved claim that the maximum of the disturbed ball is in X, or an explicit assumption ensuring that the ball remains in X should be added.

minor comments (5)

[Section V-A, Eqs. (18) and (21)] The notation min/max for sets of vectors is used ambiguously. For instance, x^{q'}_2 = max{x^{q⋆}_2 | q⋆ ∩ Qu(q,u) ≠ ∅} selects the componentwise maximum of a set of vectors; this is well-defined only when the set has a greatest element, which is precisely the issue raised in the major comment. The paper should define the intended arg-extremum notation and state the conditions under which it exists.
[Section V-B, Eq. (26)] The text says the second inequality in (26) comes from 'equation (5)' and Lemma 1, but there is no equation (5); the intended reference is the bound ε_i ≥ ∑_j α_ij ξ_j together with Lemma 1.
[Section V-A, Theorem 4] The data-driven construction at the start of Section V assumes that D is a single interval [D, D] so that the 'maximum disturbance' is well-defined, but Theorem 4 states Assumption 1, which allows finite unions of intervals. The theorem statement should explicitly restrict to the single-interval case or explain how the maximum disturbance is selected in the union case.
[Section V-B, Theorem 5 and Assumption 6] Assumption 6 refers to sampling from intervals I^+_q(ξ), which may lie outside X; the text mentions an extended set tilde X but Theorem 5 as stated does not refer to tilde X. The statement should make explicit that data points are drawn from an extended state set tilde X with X ⊆ tilde X and I^+_q(ξ) ⊆ tilde X, and that the data-driven abstraction is defined on the appropriate state set.
[Section IV-A, footnote 3] The footnote says overlaps of measure zero are ignored 'as is done in [8]', but since the proofs rely on partition cells covering X and on the quantizer being well-defined, the treatment of overlapping boundaries should be stated more carefully, for instance by assigning boundary points to exactly one cell.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity found: the abstraction and data-driven theorems are proved from monotonicity and explicit sampling assumptions, with no fitted parameter renamed as a prediction.

full rationale

The derivation chain in Sections III-V does not reduce to its inputs by construction. Theorem 2 (U_Sigma <= S_Sigma <= L_Sigma) is proved directly from the definition of monotonicity and the interval-cell geometry: the upper-sparse transition uses the cell upper corner x^q_2 and the lower-sparse transition uses the cell lower corner x^q_1, and the ASUAS witnesses R={(x,q): x <= x^q_2} and R={(q,x): x^q_1 <= x} are verified from f-monotonicity rather than assumed. The conservativeness bound in Theorem 3 uses the user-supplied derivative bound alpha_ij and discretization size eta; no parameter is fit to the resulting precision epsilon. The data-driven abstractions in Section V are constructed from finite samples, and their soundness relations U_SigmaD <= U_Sigma and L_Sigma <= L_SigmaD are proved from the sample ordering and monotonicity; the sample-complexity bound in Proposition 2 is a standard union-bound calculation. The ASUAS relation is introduced in this paper, and citations to prior work are contextual and are not used as the proof of the central claims. The possible gap that Theorems 4 and 5 are stated under Assumption 3 but their proofs may require the monotone-partition property of Assumption 4 is a missing-hypothesis and correctness issue, not a circularity: it does not make any conclusion equivalent to an input by definition. No circular step is exhibited, so the circularity score is 0.

Assumptions & free parameters 4 free parameters · 7 assumptions · 2 invented entities

The central claim rests on monotonicity, lower-closed state spaces, interval input/disturbance sets, and user-provided derivative bounds. The data-driven extension additionally requires a known disturbance Lipschitz constant, a monotone partition (not explicitly stated), and either deterministic sampling coverage or a uniform-sampling PAC bound.

free parameters (4)

Jacobian upper bounds αij = user-chosen, e.g., α11=α12=1, α21=0, α22=1 in the vehicle example
Assumption 5; convert desired precision ε into grid width η or sampling width ξ in Theorems 3 and 5. These are not fitted to data, but they are a user-provided modeling bound that controls the conservativeness gap.
Sampling interval width ξ = user-chosen, e.g., ξ=(0.5,0.5) in the example
Assumption 6 and Theorem 5; determines the deterministic precision ε via ε ≥ α ξ. A design parameter, not data-fitted.
Discretization counts nx, nu and grid width η = e.g., 20x14, 280x60 states, 10 inputs
Space and input quantization parameters; η is related to ε by (13). Chosen by the user.
Disturbance Lipschitz constant Kd = assumed known in Remark 5
Used to bloat Qu and Ql when data are not collected under maximum disturbance; a user-provided bound.

assumptions (7)

domain assumption The system is monotone (Definition 2): f is order-preserving in state, input, and disturbance.
The entire upper/lower bounding construction in Theorems 2-5 relies on f(x1,u1,d1) ≤ f(x2,u2,d2) whenever x1≤x2, u1≤u2, d1≤d2.
domain assumption The state space X is lower closed (↓X = X).
Used in Theorem 2 proofs to ensure successors of abstract transitions remain in X; stated in Theorems 2-5.
domain assumption Input and disturbance sets are intervals or finite unions of intervals (Assumption 1).
Ensures the transition system representation (2) and the existence of minimum and maximum abstract inputs U and U.
domain assumption Continuous differentiability and known Jacobian upper bounds αij (Assumption 5).
Required by Lemma 1 and Theorems 3 and 5 to convert precision to grid or sampling width.
ad hoc to paper Monotone partition ordering (Assumption 4) is needed by the proofs of Theorems 4 and 5, but is not stated in their hypotheses.
The proofs compare cell bounds of data-derived and model-derived successors; without Assumption 4 the inequalities xq'1_1 ≤ xq'2_1 and xq'1_2 ≤ xq'2_2 do not follow. This is an unflagged assumption.
domain assumption Sampling data in intervals I^+_q(ξ) for every state-input pair, or a PAC bound on that event (Assumption 6 / Proposition 2).
Necessary for Theorem 5's deterministic precision; the probabilistic analogue uses uniform sampling and the coupon-collector bound (27).
domain assumption Data collected under maximum disturbance D (Section V-A).
Used to define K+ and K- and to bound data successors; Remark 5 relaxes this with a known Lipschitz constant.

invented entities (2)

Approximate strong upper alternating simulation (ASUAS) relation
purpose: A new behavioral relation that connects a monotone system to its abstractions using output ordering and input permissiveness.
A mathematical definition (Definition 3), not an empirical entity; no falsifiable prediction outside the theory.
Upper- and lower-sparse abstractions UΣ, LΣ, UΣD, LΣD
purpose: Finite-state approximations of the original system that bracket its behavior and enable sound refinement and impossibility certificates.
Constructs defined in Sections IV-A and V-A; their existence is the content of the theorems, not independently evidenced.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Complete Abstractions of Monotone Control Systems: From Model-based to Data-Driven Systems." pith.science (2026). https://pith.science/paper/4D7I6VAN

@misc{pith2026260806689,
  author       = {Pith},
  title        = {Pith review of: Complete Abstractions of Monotone Control Systems: From Model-based to Data-Driven Systems},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/4D7I6VAN}},
  note         = {Machine review of arXiv:2608.06689}
}

read the original abstract

In this paper, we introduce the approximate strong upper alternating simulation (ASUAS), a new behavioral relation for transition systems. Building on this relation, we construct upper- and lower-sparse abstractions for monotone systems that together form a complete abstraction pair: any controller synthesized for the upper-sparse abstraction can be refined into a controller for the original system, and the absence of a controller for the lower-sparse abstraction implies the absence of a controller for the original system. A key feature of our approach is the ability to provably tune the conservativeness gap between the two abstractions by tuning the space-discretization parameter. We further extend these results, beyond the model-based setting, to data-driven systems, where the abstraction is constructed directly from finite sampled data, without requiring an explicit system model. The theoretical results are illustrated through simulations.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

40 extracted references · 38 canonical work pages

[1]

Tabuada, Verification and control of hybrid systems: a symbolic approach

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

2009
[2]

Belta, B

C. Belta, B. Yordanov, and E. Gol, Formal methods for discrete-time dynamical systems. Springer, 2017

work page 2017
[3]

Cassandras and S

C. Cassandras and S. Lafortune, Introduction to discrete event systems . Springer Science & Business Media, 2009

work page 2009
[4]

Synthe- sis of reactive (1) designs,

R. Bloem, B. Jobstmann, N. Piterman, A. Pnueli, and Y . Sa’ar, “Synthe- sis of reactive (1) designs,” Journal of Computer and System Sciences , vol. 78, no. 3, pp. 911–938, 2012

work page 2012
[5]

An approximate simulation approach to symbolic control,

P. Tabuada, “An approximate simulation approach to symbolic control,” IEEE Transactions on Automatic Control, vol. 53, no. 6, pp. 1406–1418, 2008

work page 2008
[6]

Symbolic models for nonlinear control systems without stability assumptions,

M. Zamani, G. Pola, M. Mazo, and P. Tabuada, “Symbolic models for nonlinear control systems without stability assumptions,” IEEE Transactions on Automatic Control, vol. 57, no. 7, pp. 1804–1809, 2012

work page 2012
[7]

Compositional abstraction and safety synthesis using overlapping symbolic models,

P.-J. Meyer, A. Girard, and E. Witrant, “Compositional abstraction and safety synthesis using overlapping symbolic models,” IEEE Transactions on Automatic Control , vol. 63, no. 6, pp. 1835–1841, 2017

work page 2017
[8]

Efficient finite abstraction of mixed monotone systems,

S. Coogan and M. Arcak, “Efficient finite abstraction of mixed monotone systems,” in Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control , pp. 58–67, 2015

work page 2015

Show all 40 references

[9]

Reactive controllers for differentially flat systems with temporal logic constraints,

J. Liu, U. Topcu, N. Ozay, and R. M. Murray, “Reactive controllers for differentially flat systems with temporal logic constraints,” in IEEE Conference on Decision and Control (CDC) , pp. 7664–7670, 2012

2012
[10]

Symbolic models for a class of impulsive systems,

A. Swikir, A. Girard, and M. Zamani, “Symbolic models for a class of impulsive systems,”IEEE Control Systems Letters, vol. 5, no. 1, pp. 247– 252, 2020

2020
[11]

Symbolic control of hybrid systems from signal temporal logic specifications,

R. R. da Silva, V . Kurtz, and H. Lin, “Symbolic control of hybrid systems from signal temporal logic specifications,” Guidance, Navigation and Control, vol. 1, no. 02, p. 2150008, 2021

2021
[12]

Symbolic abstrac- tions of networked control systems,

M. Zamani, M. Mazo, M. Khaled, and A. Abate, “Symbolic abstrac- tions of networked control systems,” IEEE Transactions on Control of Network Systems, vol. 5, no. 4, pp. 1622–1634, 2017

2017
[13]

Approximately bisimilar symbolic models for nonlinear control systems,

G. Pola, A. Girard, and P. Tabuada, “Approximately bisimilar symbolic models for nonlinear control systems,” Automatica, vol. 44, no. 10, pp. 2508–2516, 2008

2008
[14]

Approximately bisimilar symbolic models for incrementally stable switched systems,

A. Girard, G. Pola, and P. Tabuada, “Approximately bisimilar symbolic models for incrementally stable switched systems,” IEEE Transactions on Automatic Control , vol. 55, no. 1, pp. 116–126, 2010

2010
[15]

Symbolic models for nonlinear time-delay systems using approximate bisimulations,

G. Pola, P. Pepe, M. D. Di Benedetto, and P. Tabuada, “Symbolic models for nonlinear time-delay systems using approximate bisimulations,” Systems & Control Letters , vol. 59, no. 6, pp. 365–373, 2010

2010
[16]

Symbolic control of stochastic systems via approximately bisimilar finite abstractions,

M. Zamani, P. M. Esfahani, R. Majumdar, A. Abate, and J. Lygeros, “Symbolic control of stochastic systems via approximately bisimilar finite abstractions,” IEEE Transactions on Automatic Control , vol. 59, no. 12, pp. 3135–3150, 2014

2014
[17]

A Lyapunov approach to incremental stability properties,

D. Angeli, “A Lyapunov approach to incremental stability properties,” IEEE Transactions on Automatic Control , vol. 47, no. 3, pp. 410–421, 2002

2002
[18]

Learning-based symbolic abstractions for nonlinear control systems,

K. Hashimoto, A. Saoud, M. Kishida, T. Ushio, and D. V . Dimarogonas, “Learning-based symbolic abstractions for nonlinear control systems,” Automatica, vol. 146, p. 110646, 2022

2022
[19]

Symbolic abstractions from data: A PAC learning approach,

A. Devonport, A. Saoud, and M. Arcak, “Symbolic abstractions from data: A PAC learning approach,” in 2021 60th IEEE Conference on Decision and Control (CDC) , pp. 599–604, IEEE, 2021

2021
[20]

Formal controller synthesis for continuous-space mdps via model-free reinforce- ment learning,

A. Lavaei, F. Somenzi, S. Soudjani, A. Trivedi, and M. Zamani, “Formal controller synthesis for continuous-space mdps via model-free reinforce- ment learning,” in 2020 ACM/IEEE 11th International Conference on Cyber-Physical Systems (ICCPS) , pp. 98–107, IEEE, 2020

2020
[21]

Robust control for dynamical systems with non-gaussian noise via formal abstractions,

T. Badings, L. Romao, A. Abate, D. Parker, H. A. Poonawala, M. Stoelinga, and N. Jansen, “Robust control for dynamical systems with non-gaussian noise via formal abstractions,” Journal of Artificial Intelligence Research, vol. 76, pp. 341–391, 2023

2023
[22]

Data-driven models of mono- tone systems,

A. Makdesi, A. Girard, and L. Fribourg, “Data-driven models of mono- tone systems,” IEEE Transactions on Automatic Control , vol. 69, no. 8, pp. 5294–5309, 2023

2023
[23]

Principles of model checking,

C. Baier and J.-P. Katoen, “Principles of model checking,” MIT press, 2008

2008
[24]

Robust abstractions for control synthesis: Completeness via robustness for linear-time properties,

J. Liu, “Robust abstractions for control synthesis: Completeness via robustness for linear-time properties,” in Proceedings of the 20th In- ternational Conference on Hybrid Systems: Computation and Control , pp. 101–110, 2017

2017
[25]

Symbolic control design for monotone systems with directed specifications,

E. S. Kim, M. Arcak, and S. A. Seshia, “Symbolic control design for monotone systems with directed specifications,” Automatica, vol. 83, pp. 10–19, 2017

2017
[26]

Directed specifications and assumption mining for monotone dynamical systems,

E. S. Kim, M. Arcak, and S. A. Seshia, “Directed specifications and assumption mining for monotone dynamical systems,” in Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, pp. 21–30, 2016. 16

2016
[27]

H. L. Smith, Monotone dynamical systems: an introduction to the theory of competitive and cooperative systems. No. 41, American Mathematical Soc., 2008

2008
[28]

Monotone control systems,

D. Angeli and E. D. Sontag, “Monotone control systems,” IEEE Trans- actions on Automatic Control , vol. 48, no. 10, pp. 1684–1698, 2003

2003
[29]

Formal methods for control of traffic flow: Automated control synthesis from finite-state transition models,

S. Coogan, M. Arcak, and C. Belta, “Formal methods for control of traffic flow: Automated control synthesis from finite-state transition models,” IEEE Control Systems Magazine , vol. 37, no. 2, pp. 109–128, 2017

2017
[30]

Decentralized monotonicity-based voltage control of dc microgrids with zip loads,

D. Zonetti, A. Saoud, A. Girard, and L. Fribourg, “Decentralized monotonicity-based voltage control of dc microgrids with zip loads,” IFAC-PapersOnLine, vol. 52, no. 20, pp. 139–144, 2019

2019
[31]

Graph-theoretic characteri- zations of monotonicity of chemical networks in reaction coordinates,

D. Angeli, P. De Leenheer, and E. Sontag, “Graph-theoretic characteri- zations of monotonicity of chemical networks in reaction coordinates,” Journal of mathematical biology , vol. 61, no. 4, pp. 581–616, 2010

2010
[32]

Algorithmic and complexity results for decompositions of biological networks into monotone subsystems,

B. DasGupta, G. A. Enciso, E. Sontag, and Y . Zhang, “Algorithmic and complexity results for decompositions of biological networks into monotone subsystems,” Biosystems, vol. 90, no. 1, pp. 161–178, 2007

2007
[33]

Approximation metrics for discrete and continuous systems,

A. Girard and G. J. Pappas, “Approximation metrics for discrete and continuous systems,” IEEE Transactions on Automatic Control , vol. 52, no. 5, pp. 782–798, 2007

2007
[34]

Multi-layered abstraction-based controller synthesis for continuous-time systems,

K. Hsu, R. Majumdar, K. Mallik, and A.-K. Schmuck, “Multi-layered abstraction-based controller synthesis for continuous-time systems,” in International Conference on Hybrid Systems: Computation and Control , pp. 120–129, 2018

2018
[35]

ε-approximation of differential inclusions,

A. Puri, V . Borkar, and P. Varaiya, “ ε-approximation of differential inclusions,” in International Hybrid Systems Workshop , pp. 362–376, Springer, 1995

1995
[36]

Contract-based design of symbolic controllers for safety in distributed multiperiodic sampled- data systems,

A. Saoud, A. Girard, and L. Fribourg, “Contract-based design of symbolic controllers for safety in distributed multiperiodic sampled- data systems,” IEEE Transactions on Automatic Control , vol. 66, no. 3, pp. 1055–1070, 2020

2020
[37]

Lazy controller synthesis for monotone transition systems and directed safety specifications,

E. Ivanova, A. Saoud, and A. Girard, “Lazy controller synthesis for monotone transition systems and directed safety specifications,” Auto- matica, vol. 135, p. 109993, 2022

2022
[38]

Data-driven reachable set computation us- ing adaptive Gaussian process classification and Monte Carlo methods,

A. Devonport and M. Arcak, “Data-driven reachable set computation us- ing adaptive Gaussian process classification and Monte Carlo methods,” in Proceedings 2020 American Control Conference (ACC) , pp. 2629– 2634, IEEE, 2020

2020
[39]

Saoud, Compositional and Efficient Controller Synthesis for Cyber- Physical Systems

A. Saoud, Compositional and Efficient Controller Synthesis for Cyber- Physical Systems. PhD thesis, Universit ´e Paris Saclay, 2019

2019
[40]

Assume-guarantee contracts for continuous-time systems,

A. Saoud, A. Girard, and L. Fribourg, “Assume-guarantee contracts for continuous-time systems,” Automatica, vol. 134, p. 109910, 2021

2021

Pith tools

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

[1] [1]

Tabuada, Verification and control of hybrid systems: a symbolic approach

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

2009

[2] [2]

Belta, B

C. Belta, B. Yordanov, and E. Gol, Formal methods for discrete-time dynamical systems. Springer, 2017

work page 2017

[3] [3]

Cassandras and S

C. Cassandras and S. Lafortune, Introduction to discrete event systems . Springer Science & Business Media, 2009

work page 2009

[4] [4]

Synthe- sis of reactive (1) designs,

R. Bloem, B. Jobstmann, N. Piterman, A. Pnueli, and Y . Sa’ar, “Synthe- sis of reactive (1) designs,” Journal of Computer and System Sciences , vol. 78, no. 3, pp. 911–938, 2012

work page 2012

[5] [5]

An approximate simulation approach to symbolic control,

P. Tabuada, “An approximate simulation approach to symbolic control,” IEEE Transactions on Automatic Control, vol. 53, no. 6, pp. 1406–1418, 2008

work page 2008

[6] [6]

Symbolic models for nonlinear control systems without stability assumptions,

M. Zamani, G. Pola, M. Mazo, and P. Tabuada, “Symbolic models for nonlinear control systems without stability assumptions,” IEEE Transactions on Automatic Control, vol. 57, no. 7, pp. 1804–1809, 2012

work page 2012

[7] [7]

Compositional abstraction and safety synthesis using overlapping symbolic models,

P.-J. Meyer, A. Girard, and E. Witrant, “Compositional abstraction and safety synthesis using overlapping symbolic models,” IEEE Transactions on Automatic Control , vol. 63, no. 6, pp. 1835–1841, 2017

work page 2017

[8] [8]

Efficient finite abstraction of mixed monotone systems,

S. Coogan and M. Arcak, “Efficient finite abstraction of mixed monotone systems,” in Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control , pp. 58–67, 2015

work page 2015