A symbolic approach to the self-triggered design for networked control systems

Adnane Saoud; Dimos V. Dimarogonas; Kazumune Hashimoto; Masako Kishida; Toshimitsu Ushio

REVIEW 2 major objections 3 minor 20 references

A symbolic approach to the self-triggered design for networked control systems

T0 review · 2 major / 3 minor · reviewed 2026-08-14 · deepseek-v4-flash

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

Pith's one-line read Self-triggered control proven via symbolic reachability games

desk verdict A genuinely new abstraction for self-triggered control, but the proof of the main theorem has a real gap; worth refereeing, not ready as is. read the letter →

arxiv 1908.04750 v1 pith:XUFBB5WY submitted 2019-08-10 math.OC math.DS

Kazumune Hashimoto , Adnane Saoud , Masako Kishida , Toshimitsu Ushio , Dimos V. Dimarogonas This is my paper · ORCID

classification math.OCmath.DS MSC 93C5593B0393C6568Q60

keywords self-triggeredcontrolsymbolicmodelsreachabilityandsafetynetworkedsystemsapproximatealternatingsimulationgamenonlinearnon-convexsets

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 proposes a way to synthesize self-triggered controllers for nonlinear discrete-time control systems that must reach a target while never leaving a safety set, even when the safety set is non-convex. The approach builds a finite symbolic model of the system by quantizing states and inputs and bounding how far trajectories can drift over a fixed horizon, then solves a reachability game on that model. Winning abstract states are refined back to the original system: a concrete state quantizes to a winning abstract state, and the controller applies the abstract input and waits the abstract time. The paper proves that if every initial state lies in the winning region PS, the refined controller guarantees finite-time reachability and safety. The only assumption on the plant is Lipschitz continuity, so no stability or contraction condition is needed.

What carries the argument

The load-bearing object is the symbolic model of Definition 5, parameterized by quantization parameters ηx, ηu, a maximum inter-communication step Mmax, and precision ε≥ηx. Its transitions are defined by over-approximating the reachable tube: an abstract successor x~+ is allowed if it lies in the ball of radius L_x^m ε + ηx around φ(x~, u~, m), the true state reached from the abstract state under constant input. This makes R(ε) = {(x~,x): ‖x~ - x‖ ≤ ε} a strong ε-ASR without requiring stability. On top of the symbolic model, Algorithm 1 iteratively computes the set ~PS of abstract states from which the target is reachable within the safety set; the controller (7) chooses inputs that strictly decrease the layer L(x~), and (8) refines this to concrete states. The mechanism that carries the argument is the combination of the simulation relation, which transfers winning abstract trajectories to concrete ones, and the ε-shrinking of XS and XF, which converts abstract safety into concrete safety.

What would settle it

Simulate the refined controller for any Lipschitz system with verified X0 ⊆ PS; a single trajectory that exits XS before reaching XF would refute Theorem 1.

Watch

Extended reading notes

Core claim

The central claim is Theorem 1: given the augmented transition system of a Lipschitz nonlinear plant, its quantized symbolic model, and a strong ε-approximate alternating simulation relation between them, the reachability-game winning set ~PS can be transferred to the plant. Define PS as all concrete states x such that some nearest abstract state is in ~PS. If the initial set X0 lies inside PS, then the controller that picks a winning abstract state nearest to the current concrete state, applies the corresponding constant input for the corresponding waiting time, is valid: every induced trajectory enters the target set in finite time and never leaves the safety set. The proof works by inductively matching each concrete transition to an abstract transition in the winning set, with the simulation relation ensuring the abstract state stays in the shrunk safety set ~XS while the concrete state stays in XS.

Load-bearing premise

The guarantee collapses if X0 ⊈ PS: the paper gives no constructive procedure for choosing the quantization and precision parameters to ensure this inclusion, and for a given plant the winning set can be empty.

Editorial extensions

If this is right

The synthesis works for non-convex safety sets, so obstacle-filled environments in robot motion planning are directly admissible.
No Lyapunov or incremental stability assumption is needed; Lipschitz continuity suffices, expanding the class of plants beyond earlier self-triggered designs.
Communication is aperiodic: the controller outputs both the input and the waiting time, reducing the number of transmissions compared to periodic control (109 to 6 in the example).
The guarantee is conditional on X0 ⊆ PS; when the condition fails, one can still restrict to X0 ∩ PS and obtain a valid controller for that subset.
Because the symbolic model is finite, the synthesis terminates, so the same algorithm can be implemented for any discrete-time Lipschitz plant once the parameters are fixed.

Reading between the lines

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

The condition X0 ⊆ PS is not only a proof artifact; it suggests a practical design loop where one coarsens ηx, ηu until PS covers X0, at the cost of exponential growth of the abstract state space. A dual strategy—fixing the controller and learning the coarsest admissible quantization—might be derived from the same simulation bounds.
The layer function L(x~) computed by Algorithm 1 could be reused as a runtime Lyapunov-like certificate for the closed loop, giving a data structure that monitors the remaining time-to-target without additional computation.
The over-approximation radius ε_m = L_x^m ε + ηx grows exponentially with the waiting time m, so long inter-communication steps are penalized by conservatism. This suggests an inherent trade-off between communication reduction and achievable precision that could be formalized as an optimization over Mmax.
For systems with large Lipschitz constants, the method may produce an empty ~PS even when a valid controller exists, so a natural testable extension is a parameter-adaptive scheme that locally refines the lattice only near the winning frontier.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

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

Read this one if you care about symbolic-model synthesis for networked control. The genuinely new piece is the augmented transition system: the controller chooses the inter-communication interval m together with u, and the symbolic model is built over the joint (u,m) decisions with precision ε_m = L_x^m ε + η_x. That is a natural but non-obvious move, and it is what lets them treat non-convex safety sets without stability assumptions. I agree with the reader that Lemma 2 and the engineering of the abstraction are sound; the quantization error propagation through the Lipschitz bound is clean.

The soft spots are two. First, the main theorem's proof has a gap, and the stress-test note is right. At each round the concrete controller (8) looks at Nearest_{~P_S}(x_k), but the induction in Theorem 1 uses the abstract successor produced by the simulation relation. These need not be the same abstract state, and nothing forces the rank to decrease when you switch to the nearest one. The rank function can jump upward between neighboring lattice states, so the memoryless controller may not follow a winning abstract trajectory. This is a load-bearing gap: X_0 ⊆ P_S plus a valid abstract controller is not enough, as written, to guarantee finite-time reachability. It is fixable — use memory, or select the successor as part of the control decision — but the authors need to say which.

Second, the design relies on the condition X_0 ⊆ P_S, and there is no constructive way to choose η_x, η_u, ε, M_max to make it hold. The paper admits this in Remarks 1-2 and lists the parameter search as future work. That is a practical rather than logical weakness, but it matters because the only numerical example took 20,760 seconds for a two-dimensional system and no code or data is included to reproduce it.

Citation pattern is fine; the self-citations are on point. I would not desk-reject this. The construction is novel and the reachability-game formulation is competent. But the proof gap in Theorem 1 must be fixed before the result can be accepted, and the parameter-selection issue should at least get a systematic discussion. A serious referee would be doing useful work.

Referee Report

2 major / 3 minor

Summary. The paper proposes a symbolic-model method for synthesizing self-triggered controllers for nonlinear discrete-time systems subject to reachability and safety specifications. It constructs an augmented transition system for the plant, quantizes it to a finite symbolic model, establishes a strong approximate alternating simulation relation (Lemma 2), solves a reachability game on the abstraction (Algorithm 1) to obtain an abstract winning set and a rank function, and then refines the abstract controller to a memoryless self-triggered controller via Eq. (8). Theorem 1 claims that if all concrete initial states lie within precision ε of the abstract winning set, the refined controller guarantees finite-time reachability of the target set and invariance of the safety set. A numerical vehicle example illustrates the approach and reports aperiodic communication.

Significance. If the central theorem were correct, the paper would contribute a useful abstraction-based synthesis method for self-triggered control with non-convex safety sets, requiring only Lipschitz continuity rather than stability or contractivity assumptions. The construction of the symbolic model and the proof of Lemma 2 are technically sound, and Algorithm 1 is a standard and appropriate fixpoint scheme for the abstract reachability-safety game. The numerical example demonstrates the intended behavior. However, the refinement step in Theorem 1 is not established as written: the memoryless nearest-state selection can break the rank-decrease argument on which the finite-time guarantee rests. The flaw is repairable, but the paper's main guarantee currently lacks a valid proof.

major comments (2)

[Section IV, Theorem 1 (Eq. (8))] The proof of Theorem 1 has an invalid induction step. In the first step the proof picks ~x_k0 ∈ Nearest_{~P_S}(x_k0) with rank N and uses the strong ε-ASR to obtain an existential abstract successor ~x_k1 ∈ P(N−1) that is related to the concrete successor x_k1. It then says to repeat the procedure from k1. The repeat step, however, must choose Nearest_{~P_S}(x_k1), and nothing in Definition 5, Eq. (7), or Eq. (8) guarantees that this nearest point has rank at most N−1; the rank function L on the finite lattice can vary arbitrarily between nearby abstract states, so the selected point may have rank N or larger. Consequently the sequence of abstract states actually used by the memoryless controller (8) need not be a trajectory of ~ΣA with decreasing L, and Lemma 3 does not apply recursively. A correct refinement would need to choose, for example, an abstract state of minimal rank among those within ε of the concrete state, or to carry the previous abstract state as memory.
[Section IV, Definition 1 and Eq. (8)] Even if the rank of the nearest abstract state were controlled at the first step, the controller C(x) in Eq. (8) is the union of ~C(~x) over all ~x ∈ Nearest_{~P_S}(x). Since different nearest points can have different ranks, a controlled trajectory in the sense of Definition 1, which quantifies over all possible induced trajectories, could at every communication instant select an action coming from a high-rank nearest point. The proof of Theorem 1 silently fixes one abstract state, but the nondeterminism in (8) is not resolved by the controller definition.

minor comments (3)

[Remark 2] The sentence 'Even though X0 ⊈PS does not hold' is confusing and should presumably read 'Even if X0⊆PS does not hold, one might still be interested...'.
[Proof of Lemma 3] The input pair (u′, m′) is introduced in the proof, but the safety condition is later written with (u, m) without primes; this notational slip should be corrected.
[Section V] The phrase 'with 6 number of communication times' should be reworded, for example as 'with 6 communication events'.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the abstraction, reachability game, and controller refinement are derived from stated Lipschitz assumptions and proved locally, not fitted to data or imported from the authors' prior work.

full rationale

The derivation chain is self-contained. Lemma 2 proves that the relation R(ε) = {(˜x, x) : ||˜x − x|| ≤ ε} is a strong ε-ASR from the symbolic model ~Σ^ε_A to Σ_A directly from Assumption 1 (Lipschitz continuity), the quantization structure, and the definition of ~G_A; no constant is fitted to data and no empirical prediction is renamed. Algorithm 1 computes the winning set ~P_S by a standard fixed-point reachability game on the finite abstract state space, and controller (7) is defined purely from the rank L computed by that iteration. Theorem 1 then transfers the abstract reachability/safety guarantee to the concrete system through the ε-ASR, under the explicit hypothesis X0 ⊆ P_S; this hypothesis is an assumption on the initial set, not a hidden restatement of the conclusion. The self-citations [6], [7], and [9] appear only as background comparisons in the introduction and are not load-bearing for the synthesis proof; the central simulation-relation framework is credited to [16] and is re-proved in Lemma 2. The authors' own Remarks 1 and 2, plus the conclusion, acknowledge that no constructive procedure is given for choosing ηx, ηu so that X0 ⊆ P_S holds; this is a limitation of the method, not a circular reduction. Finally, the skeptical concern about the induction step in Theorem 1—that the nearest abstract state at the next communication may not inherit a smaller rank—is a potential proof-soundness gap, not a circularity, because it does not show that the theorem assumes its own conclusion.

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

The central claim rests on user-chosen quantization parameters and the standard symbolic-control framework; no new physical or mathematical entities are postulated. The free parameters are all design choices, not fitted values, and they enter only through the sufficient condition X0 ⊆ PS.

free parameters (4)

ηx (state quantization parameter) = 1 (in the example)
State lattice spacing; chosen by the user. The theorem requires ε ≥ ηx, and the condition X0 ⊆ PS depends critically on this choice.
ηu (input quantization parameter) = 50 (in the example)
Control input lattice spacing; chosen by the user. Coarser ηu reduces the number of abstract actions and may make the winning set smaller.
ε (precision of the simulation relation) = 1 (in the example, equal to ηx)
Radius of the approximate alternating simulation relation; must satisfy ε ≥ ηx. Larger ε makes the abstraction coarser while ensuring the refinement safety margin.
Mmax (maximum inter-communication step) = 30 (in the example)
Bounds the abstract action set M = N1:Mmax. Larger Mmax gives more scheduling flexibility but increases the state-space and Pre computation.

assumptions (3)

domain assumption Assumption 1: f is Lipschitz continuous in x with constant Lx.
Used in Lemma 1 and Lemma 2 to propagate the abstraction error as ε_m = Lx^m ε + ηx; without it the symbolic transition bounds do not hold.
domain assumption X0, U, XS, XF are compact sets.
Guarantees the quantized sets X̃, Ũ, X̃S, X̃F are finite, so Algorithm 1 terminates; standard in abstraction-based synthesis.
domain assumption The notion of strong ε-ASR and the refinement property (controller validity transfers from abstraction to concrete system) from [16] and [10].
The paper proves the specific instance for its symbolic model in Lemma 2 and Theorem 1, but the framework and the game-based synthesis are taken as background results from the cited literature.

how reviews work

0 comments

Cite this review

Pith. "Pith review of A symbolic approach to the self-triggered design for networked control systems." pith.science (2026). https://pith.science/paper/XUFBB5WY

@misc{pith2026190804750,
  author       = {Pith},
  title        = {Pith review of: A symbolic approach to the self-triggered design for networked control systems},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/XUFBB5WY}},
  note         = {Machine review of arXiv:1908.04750}
}

read the original abstract

In this paper, we investigate novel self-triggered controllers for nonlinear control systems with reachability and safety specifications. To synthesize the self-triggered controller, we leverage the notion of symbolic models, or abstractions, which represent abstracted expressions of control systems. The symbolic models will be constructed through the concepts of approximate alternating simulation relations, based on which, and by employing a reachability game, the self-triggered controller is synthesized. We illustrate the effectiveness of the proposed approach through numerical simulations.

Figures

Figures reproduced from arXiv: 1908.04750 by the authors.

**Figure 1.** Networked Control System. B. Self-triggered strategy Let us now provide the overview of the control strategies. First, let k`, ` ∈ N≥0 with k0 = 0, k`+1 > k`, ∀` ∈ N≥0 be the communication time steps when the information is exchanged between the plant and the controller. In this paper, we employ a self-triggered strategy [1], which means that the controller is defined as a mapping from the state to the corresponding… view at source ↗

**Figure 2.** Geometry of the road based on the road grade profile [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗

**Figure 3.** Simulation results. The upper figure illustrates some trajectories by [PITH_FULL_IMAGE:figures/full_fig_p006_3.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

20 extracted references · 17 canonical work pages

[1]

An introduction to event-triggered and self-triggered control,

W. P. M. H. Heemels, K. H. Johansson, and P. Tabuada, “An introduction to event-triggered and self-triggered control,” in Proceedings of the 51st IEEE Conference on Decision and Control (IEEE CDC) , 2012, pp. 3270–3285

2012
[2]

A survey of event-based strate- gies on control and estimation,

Q. Liu, Z. Wang, X. He, and D. Zhou, “A survey of event-based strate- gies on control and estimation,” Systems Science & Control Engineering, vol. 2, no. 1, pp. 90–97, 2014

work page 2014
[3]

A survey on recent advances in event-triggered communication and control,

C. Peng and F. Li, “A survey on recent advances in event-triggered communication and control,” Information Sciences , vol. 457, pp. 113– 125, 2018

2018
[4]

Self-triggered control for sampled-data systems using reachability analysis,

M. A. Khatib, A. Girard, and T. Ding, “Self-triggered control for sampled-data systems using reachability analysis,” in Proceedings of 20th IFAC World Congress, 2017, pp. 7881–7886

work page 2017
[5]

Event-triggered algorithms for continuous- time systems based on reachability analysis,

N. Meslem and C. Prieur, “Event-triggered algorithms for continuous- time systems based on reachability analysis,” in Proceedings of 52nd IEEE Confernece on Decision and Control , 2013

work page 2013
[6]

Aperiodic sampled- data control via explicit transmission mapping: a set-invariance ap- proach,

K. Hashimoto, S. Adachi, and D. V . Dimarogonas, “Aperiodic sampled- data control via explicit transmission mapping: a set-invariance ap- proach,” IEEE Transactions on Automatic Control , vol. 63, no. 10, pp. 3523–3530, 2018

work page 2018
[7]

Self-triggered control for constrained systems: a contractive set-based approach,

K. Hashimoto, S. Adachi, and D. V . Dimarogonas, “Self-triggered control for constrained systems: a contractive set-based approach,” in Proceedings of 2017 American Control Conference , 2017, pp. 1011– 1016

work page 2017
[8]

Event-triggered and self- triggered control for linear systems based on reachable sets,

F. Brunner, W. Heemels, and F. Allgower, “Event-triggered and self- triggered control for linear systems based on reachable sets,”Automatica, vol. 101, pp. 15–26, 2019

work page 2019

Show all 20 references

[9]

Synthesizing communication plans for reachability and safety speciﬁcations,

K. Hashimoto and D. V . Dimarogonas, “Synthesizing communication plans for reachability and safety speciﬁcations,” IEEE Transactions on Automatic Control, (to appear)
[10]

Tabuada, Veriﬁcation and Control of Hybrid Systems – A Symbolic Approach, Springer, 2009

P. Tabuada, Veriﬁcation and Control of Hybrid Systems – A Symbolic Approach, Springer, 2009

2009
[11]

Symbolic models for incrementally stable switched systems with aperiodic time sampling,

Z. Kader, A. Girard, and A. Saoud, “Symbolic models for incrementally stable switched systems with aperiodic time sampling,” in Proceedings of 6th IFAC Conference on Analysis and Design of Hybrid Systems , 2018

2018
[12]

A formal trafﬁc characterization of LTI event-triggered control systems,

A. S. Kolarijani and M. Mazo Jr., “A formal trafﬁc characterization of LTI event-triggered control systems,” IEEE Transactions on Control of Network Systems, vol. 5, no. 1, pp. 274–283, 2018

2018
[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]

Optimal multirate sampling in symbolic models for incrementally stable switched systems,

A. Saoud and A. Girard, “Optimal multirate sampling in symbolic models for incrementally stable switched systems,” Automatica, vol. 98, pp. 58–65, 2018

2018
[15]

Symbolic models for nonlinear control systems without stability assumptions,

M. Zamani, G. Pola, M. Mazo Jr., 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

2012
[16]

Design of symbolic con- trollers for networked control systems,

A. Borri, G. Pola, and M. D. D. Benedetto, “Design of symbolic con- trollers for networked control systems,”IEEE Transactions on Automatic Control, 2019 (to appear)

2019
[17]

Symbolic approximate time-optimal control,

M. Mazo Jr. and P. Tabuada, “Symbolic approximate time-optimal control,” Systems & Control Letters , vol. 60, no. 4, pp. 256–263, 2011

2011
[18]

Symbolic abstrac- tions of networked control systems,

M. Zamani, M. Mazo Jr., 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, 2018

2018
[19]

Compositional abstraction-based synthesis for cascade discrete-time control systems,

A. Saoud, P. Jagtap, M. Zamani, and A. Girard, “Compositional abstraction-based synthesis for cascade discrete-time control systems,” in Proceedings of 6th IFAC Conference on Analysis and Design of Hybrid Systems, 2018

2018
[20]

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, 2018

2018

Pith tools

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

[1] [1]

An introduction to event-triggered and self-triggered control,

W. P. M. H. Heemels, K. H. Johansson, and P. Tabuada, “An introduction to event-triggered and self-triggered control,” in Proceedings of the 51st IEEE Conference on Decision and Control (IEEE CDC) , 2012, pp. 3270–3285

2012

[2] [2]

A survey of event-based strate- gies on control and estimation,

Q. Liu, Z. Wang, X. He, and D. Zhou, “A survey of event-based strate- gies on control and estimation,” Systems Science & Control Engineering, vol. 2, no. 1, pp. 90–97, 2014

work page 2014

[3] [3]

A survey on recent advances in event-triggered communication and control,

C. Peng and F. Li, “A survey on recent advances in event-triggered communication and control,” Information Sciences , vol. 457, pp. 113– 125, 2018

2018

[4] [4]

Self-triggered control for sampled-data systems using reachability analysis,

M. A. Khatib, A. Girard, and T. Ding, “Self-triggered control for sampled-data systems using reachability analysis,” in Proceedings of 20th IFAC World Congress, 2017, pp. 7881–7886

work page 2017

[5] [5]

Event-triggered algorithms for continuous- time systems based on reachability analysis,

N. Meslem and C. Prieur, “Event-triggered algorithms for continuous- time systems based on reachability analysis,” in Proceedings of 52nd IEEE Confernece on Decision and Control , 2013

work page 2013

[6] [6]

Aperiodic sampled- data control via explicit transmission mapping: a set-invariance ap- proach,

K. Hashimoto, S. Adachi, and D. V . Dimarogonas, “Aperiodic sampled- data control via explicit transmission mapping: a set-invariance ap- proach,” IEEE Transactions on Automatic Control , vol. 63, no. 10, pp. 3523–3530, 2018

work page 2018

[7] [7]

Self-triggered control for constrained systems: a contractive set-based approach,

K. Hashimoto, S. Adachi, and D. V . Dimarogonas, “Self-triggered control for constrained systems: a contractive set-based approach,” in Proceedings of 2017 American Control Conference , 2017, pp. 1011– 1016

work page 2017

[8] [8]

Event-triggered and self- triggered control for linear systems based on reachable sets,

F. Brunner, W. Heemels, and F. Allgower, “Event-triggered and self- triggered control for linear systems based on reachable sets,”Automatica, vol. 101, pp. 15–26, 2019

work page 2019