arXiv subjects

Sadek Belamfedel Alaoui

Publications and source records attributed to Sadek Belamfedel Alaoui.

6 recordsLinked to original sources

arXiv2026

Nagumo Theorem For Constrained Differential Inclusions: Transversal Intersection and Set-Map Regularity

We study a solution-independent condition certifying forward invariance of closed sets for constrained continuous-time systems. The proposed condition is only necessary in general, we establish its sufficiency under three assumptions. These assumptions, related to critical boundary points, restrict the dynamics and enforce mild transversality between the set constraining the dynamics and the set to render forward invariant. When the boundary of the latter set is within the interior of the former, we recover the well-known Nagumo characterization of forward invariance. We further simplify the proposed framework when the considered sets are regular; namely, by considering finitely-represented (resp., polytopic) sets-defined as the intersection of sublevel sets of smooth (resp., linear) functions-yielding conditions directly checkable from the defining functions. These conditions are shown to reduce to finite linear matrix inequalities (LMI)s under polytopic dynamics. These results carry important impacts on safety verification/falsification, reachability analysis, and compositional analysis and design for both constrained and hybrid systems.

math.OC↗

arXiv2026

Invariance is Compositional for Continuous-time Systems: From Sleekness to Lebesgue Density

This work establishes the first bidirectional compositional invariance result: robust forward invariance of a global Cartesian product set is shown to be equivalent to robust forward invariance of each local subsystem under coupling inputs from its neighbors. To facilitate this, we introduce the notion of tangential Lebesgue-density, a new condition that is weaker than classical sleekness but sufficient to ensure that the product of individual tangent cones equals the tangent cone of the product set. This equivalence reduces the curse of dimensionality by allowing the verification of a high-dimensional global system to be decomposed into a series of local sub-checks. The framework's scalability is demonstrated through a DC microgrid numerical example, confirming that the verification complexity grows only linearly with the number of subsystems.

eess.SY↗

arXiv2024

How to discretize continuous state-action spaces in Q-learning: A symbolic control approach

Q-learning is widely recognized as an effective approach for synthesizing controllers to achieve specific goals. However, handling challenges posed by continuous state-action spaces remains an ongoing research focus. This paper presents a systematic analysis that highlights a major drawback in space discretization methods. To address this challenge, the paper proposes a symbolic model that represents behavioral relations, such as alternating simulation from abstraction to the controlled system. This relation allows for seamless application of the synthesized controller based on abstraction to the original system. Introducing a novel Q-learning technique for symbolic models, the algorithm yields two Q-tables encoding optimal policies. Theoretical analysis demonstrates that these Q-tables serve as both upper and lower bounds on the Q-values of the original system with continuous spaces. Additionally, the paper explores the correlation between the parameters of the space abstraction and the loss in Q-values. The resulting algorithm facilitates achieving optimality within an arbitrary accuracy, providing control over the trade-off between accuracy and computational complexity. The obtained results provide valuable insights for selecting appropriate learning parameters and refining the controller. The engineering relevance of the proposed Q-learning based symbolic model is illustrated through two case studies.

eess.SY↗

arXiv2024

Contract-Based Design for Hybrid Dynamical Systems and Invariance Properties

This work establishes fundamental principles for verifying contract for interconnected hybrid systems. When system's hybrid arcs conform to the contract for a certain duration but subsequently violate it, the composition of hybrid dynamical systems becomes challenging. The objective of this work is to analyze the temporal satisfaction of the contract, allowing us to reason about the compositions that do not violate the contract up to a certain point in a hybrid time. Notions of weak and strong satisfaction of an assume-guarantee contract are introduced. These semantics permits the compositional reasoning on hybrid systems of varying complexity depending on the interconnection's type, feedback or cascade. The results show that both semantics are compatible with cascade composition, while strong semantic is required for feedback composition. Moreover, we have shown how one can go from weak to strong contract satisfaction. Finally, we have studied a particular class of hybrid systems and we have shown that the concept of forward (pre-)invariant relative to a contract makes it possible to deal with feedback compositions. These results are demonstrated throughout the paper with simple numerical examples.

eess.SY↗

arXiv2023

Symbolic Models for Interconnected Impulsive Systems

In this paper, we present a compositional methodology for constructing symbolic models of nonlinear interconnected impulsive systems. Our approach relies on the concept of "alternating simulation function" to establish a relationship between concrete subsystems and their symbolic models. Assuming some small-gain type conditions, we develop an alternating simulation function between the symbolic models of individual subsystems and those of the nonlinear interconnected impulsive systems. To construct symbolic models of nonlinear impulsive subsystems, we propose an approach that depends on incremental input-to-state stability and forward completeness properties. Finally, we demonstrate the advantages of our framework through a case study.

eess.SY↗

arXiv2022

A two dimensional fluid model for TCP/AQM analysis

This work proposes a new mathematical model for the TCP/AQM system that aims to improve the accuracy of existing fluid models, especially with respect to the sequential events that occur in the network. The analysis is based on the consideration of two time bases, one at the queue's router level and the other at the congestion window level, which leads to the derivation of a new nonlinear two-dimensional fluid model for Internet congestion control. To avoid the difficult task of assessing stability of a 2D nonlinear dynamic model, we perform a local stability analysis of a 2D linear TCP AQM model. By constructing a new two dimensional second order Bessel Legendre Lyapunov functional, new matrix inequalities are derived to evaluate the stability of the 0-input system and to synthesize a feedback controller. Finally, two Internet traffic scenarios, with state space matrices for replicability, are presented, demonstrating the validity of the theoretical results.

eess.SY↗