arXiv subjects

Abolfazl Lavaei

Publications and source records attributed to Abolfazl Lavaei.

At least 19 recordsLinked to original sources

arXiv2026

From Noisy Data to Hierarchical Control: A Model-Order-Reduction Framework

This paper develops a direct data-driven framework for constructing reduced-order models (ROMs) of discrete-time linear dynamical systems with unknown dynamics and process disturbances. The proposed scheme enables controller synthesis on the ROM and its refinement to the original system via an interface function designed using noisy data. To achieve this, the notion of simulation functions (SFs) is employed to establish a formal relation between the original system and its ROM, yielding a quantitative bound on the mismatch between their output trajectories. To construct such relations and interface functions, we rely on data collected from the unknown system. In particular, using noise-corrupted input-state data gathered along a single trajectory of the system, and without identifying the original dynamics, we propose data-dependent conditions, cast as a semidefinite program, for the simultaneous construction of ROMs, SFs, and interface functions. Through a case study, we demonstrate that data-driven controller synthesis on the ROM, combined with controller refinement via the interface function, enables the satisfaction of complex logic specifications.

eess.SY↗

arXiv2026

Data-Driven Formal Methods for Complex Dynamical Systems: A Survey

Data-driven approaches with formal guarantees have recently emerged as a powerful means for the verification and controller synthesis of complex dynamical systems. Interest in these methods is rapidly growing, as system models are often unavailable in practice, and challenges such as nonlinear behavior, uncertainty, and the curse of dimensionality typically render accurate modeling infeasible. These difficulties motivate leveraging limited data collected from the system while still providing formal guarantees on its overall behavior. The community has therefore proposed a few hundred articles on the development of data-driven frameworks that enable the formal verification and synthesis of dynamical systems without explicit models, addressing complex specifications beyond stability. Despite this rapid growth, existing results remain scattered and lack a coherent organization, limiting a clear understanding of their principles, distinctions, and practical potential. This survey fills this gap by providing a comprehensive overview of these data-driven methods for both deterministic and stochastic dynamical systems. We structure the literature around three main methodological pillars in formal methods: (in)finite-abstraction-based techniques, functional certificate approaches, such as control barrier certificates, and compositional methods. For each of these approaches, we classify the resulting data-driven guarantees into three main categories: (i) statistical guarantees grounded in probably approximately correct and scenario-based frameworks, (ii) guarantees derived from Lipschitz continuity, and (iii) guarantees exploiting structural properties. While the literature on deterministic systems is considerably richer, we also devote particular attention to the stochastic counterpart, highlighting the inherent differences and challenges that arise compared to the deterministic case.

eess.SY↗

arXiv2026

Safe Packetized Control for Stochastic Constrained Networked Systems

This work develops a formal framework for the synthesis of packetized safety controllers for discrete-time polynomial stochastic networked control systems (dt-PSNCS) operating under communication constraints, including uplink delays (plant-to-controller) and downlink packet losses (controller-to-actuator). In this setting, the controller is deployed remotely and exchanges information with the plant over an imperfect wireless communication network. Our proposed approach treats the downlink channel as an erasure channel, with packet losses characterized by an independent Bernoulli process. To systematically manage both uplink delays and downlink packet loss, we first introduce a buffer collocated with the plant that accommodates the packetized safety control (PSC) mechanism. We augment the plant and buffer states into a unified augmented-state representation that accurately captures the system evolution in the presence of communication imperfections. Our proposed framework synthesizes safety controllers based on control barrier certificates (CBCs), providing probabilistic safety guarantees that remain robust in the presence of both communication delays and packet losses. To achieve this, we reformulate the safety constraints as a sum-of-squares (SOS) optimization program, thereby facilitating the systematic construction of CBCs and their corresponding safety controllers. We validate the proposed framework through three (physical) case studies, demonstrating its effectiveness and practical applicability.

eess.SY↗

arXiv2026

Data-Driven Stabilizing Controller Design for Linear Infinite Networks

We propose a direct data-driven method for controller synthesis of infinite networks composed of unknown linear time-invariant subsystems. Using a single set of noise-corrupted input-state trajectories collected from each subsystem, and provided that certain linear matrix inequalities hold, each subsystem is rendered exponentially input-to-state stable (eISS) by locally constructing an eISS control Lyapunov function together with an exponentially input-to-state stabilizing feedback controller. We then compose these local components under a compositional small-gain condition in infinite-dimensional spaces to obtain a global control Lyapunov function and an associated stabilizing controller, ensuring uniform global exponential stability of the infinite network. The approach is validated on a physical case study with unknown dynamics.

eess.SY↗

arXiv2026

Data-Driven Adaptive Second-Order Sliding Mode Control with Noisy Data

This paper proposes a data-driven approach to designing adaptive suboptimal second-order sliding mode (ASSOSM) controllers for a class of single-input nonlinear systems with partially unknown dynamics, subject to both matched and unmatched disturbances. We first view the system as comprising two coupled dynamics, referred to as the upper and lower dynamics, with the last state serving as a virtual input to the upper dynamics. The proposed control-design methodology then follows a two-stage procedure: (i) designing a virtual state-feedback control law for the upper dynamics and (ii) synthesizing an ASSOSM controller for the full-order system. To this end, we collect noise-corrupted data from the system throughout a finite-time experiment. We then formulate a data-dependent condition, whose feasibility enables the design of a virtual state-feedback control law that renders the closed-loop upper dynamics input-to-state stable with respect to the unmatched disturbance. Building on this virtual state-feedback control law, we subsequently propose a data-driven nonlinear sliding variable, based on which an ASSOSM controller is designed for the full-order system. The state trajectories of the resulting closed-loop system are semiglobally ultimately bounded (S-GUB), with the ultimate bound explicitly depending on the magnitude of the unmatched disturbance. In particular, the control design parameters can be selected for any prescribed bounded set of initial conditions so that the state trajectories of the closed-loop system are S-GUB. Moreover, the effect of the matched disturbance is totally rejected after a finite time. The effectiveness of the proposed method is satisfactorily demonstrated in the simulation.

eess.SY↗

arXiv2026

Data-Driven Stochastic Control: Foundations and Guarantees

This work establishes a step forward in advancing data-driven trajectory-based methods for stochastic systems with unknown mathematical dynamics. In contrast to scenario-based approaches that rely on independent and identically distributed (i.i.d.) trajectories, this work develops a data-driven framework where each trajectory is gathered over a finite horizon and exhibits temporal dependence, referred to as a non-i.i.d. trajectory. To ensure safety of dynamical systems using such trajectories, the current body of literature primarily considers dynamics subject to unknown-but-bounded disturbances, which facilitates robust analysis. While promising, such bounds may be violated in practice and the resulting worst-case robust analysis tends to be overly conservative. To overcome these key challenges, this paper considers stochastic systems with unknown mathematical dynamics, influenced by process noise with arbitrary distributions. In the proposed framework, data is collected from stochastic systems under multiple realizations within a finite-horizon experiment, where each realization generates a non-i.i.d. trajectory. Leveraging the concept of stochastic control barrier certificates constructed from data, this work quantifies probabilistic safety guarantees with a certified confidence level. To achieve this, the proposed conditions are formulated as a sum-of-squares (SOS) optimization problem, relying solely on empirical average of the collected trajectories and statistical features of the process noise. The efficacy of the approach has been validated on three stochastic benchmarks with unknown models and arbitrary noise distributions. In one case study, it is shown that while no safety controller exists for the robust analysis of the system under bounded disturbances, the proposed stochastic framework yields a safety controller together with quantified probabilistic safety guarantees.

eess.SY↗

arXiv2026

Data-Efficient Control of Polynomial Systems via Physics-Guided Quadratic Constraints

This work addresses the critical challenge of guaranteeing safety for complex dynamical systems where precise mathematical models are uncertain and data measurements are corrupted by noise. We develop a physics-guided, direct data-driven framework for synthesizing robust safety controllers for discrete-time nonlinear polynomial systems that are subject to unknown-but-bounded disturbances. To do so, we introduce a notion of safety through robust control barrier certificates, which ensure avoidance of unsafe regions, offering a less conservative alternative to existing methods based on robust invariant sets. To achieve data efficiency, we further integrate physical information, formulated as quadratic constraints on system and control matrices, with observed noisy data. This integration drastically reduces data requirements, enabling robust safety analysis with significantly shorter trajectories compared to purely data-driven methods. The proposed synthesis procedure is formulated as a sum-of-squares optimization program that systematically designs the barrier and its associated controller by leveraging both collected data and underlying physical laws. The efficacy of our framework is demonstrated on three benchmark systems, confirming its ability to offer robust safety guarantees with reduced data demands.

eess.SY↗

arXiv2026

k-Inductive Neural Barrier Certificates for Unknown Nonlinear Dynamics

While conventional (k=1) discrete-time barrier certificate conditions impose strict safety constraints by requiring the function to be non-increasing at every step, k-inductive barrier certificates relax this by allowing a temporary increase -- up to k-1 times, each within a threshold $ε$ -- while maintaining overall safety, and improving flexibility. This paper leverages neural networks and constructs k-inductive neural barrier certificates (k-NBCs) for (partially) unknown nonlinear systems. While neural networks offer scalability in the design process, they lack formal guarantees, requiring additional approaches such as counterexample-guided inductive synthesis (CEGIS) with satisfiability modulo theories (SMT) for verification. However, the CEGIS-SMT framework requires knowledge of system dynamics, which is unavailable in practical settings. To address this, we leverage the generalization of the Willems et al.'s fundamental lemma, using a single state trajectory, to construct a data-driven representation of (partially) unknown models for SMT verification without sacrificing accuracy. Additionally, CEGIS-SMT further removes the constraint of restricting barrier certificates to specific function classes, such as sum-of-squares, enabling greater flexibility in their design. We validate our approach on three nonlinear case studies with (partially) unknown dynamics.

eess.SY↗

arXiv2026

Data-Driven Safety Certificates of Infinite Networks with Unknown Models and Interconnection Topologies

Infinite networks are complex interconnected systems comprising a countably infinite number of subsystems, for which no fixed upper bound on the number of participating subsystems is specified a priori since it may vary over time as agents join or leave (e.g., vehicles in traffic). In such scenarios, the presence of infinitely many subsystems within the network renders the existing analysis frameworks tailored for finite networks inapplicable to infinite ones. This paper is concerned with offering a data-driven approach, within a compositional framework, for the safety certification of infinite networks with both unknown mathematical models and unknown interconnection topologies. Given the immense computational complexity stemming from the extensive dimension of infinite networks, our approach capitalizes on the joint dissipativity-type properties of subsystems, characterized by storage certificates. We introduce innovative compositional data-driven conditions to construct a barrier certificate for the infinite network leveraging storage certificates of its unknown subsystems derived from data, while offering correctness guarantees for network safety. We demonstrate that our compositional data-driven reasoning eliminates the requirement for checking the traditional dissipativity condition, which typically mandates precise knowledge of the interconnection topology. We illustrate our data-driven results on two physical infinite networks with unknown models and interconnection topologies.

eess.SY↗

arXiv2026

A Physics-Informed Scenario Approach with Data Mitigation for Safety Verification of Nonlinear Systems

This paper develops a physics-informed scenario approach for safety verification of nonlinear systems using barrier certificates (BCs) to ensure that system trajectories remain within safe regions over an infinite time horizon. Designing BCs often relies on an accurate dynamics model; however, such models are often imprecise due to the model complexity involved, particularly when dealing with highly nonlinear systems. In such cases, while scenario approaches effectively address the safety problem using collected data to construct a guaranteed BC for the unknown dynamical system, they often require solving an optimization problem with substantial amounts of data. To address this, we propose a physics-informed scenario approach that selects data samples such that the outputs of the physics-based model and the observed data are sufficiently close. This approach guides the scenario optimization process to eliminate redundant samples and potentially reduce the required dataset size. We validate our approach through three case studies, showcasing its practical application in reducing the required data.

eess.SY↗

arXiv2026

Data-Driven Incremental GAS Certificate of Nonlinear Homogeneous Networks: A Scenario Approach with Noisy Data

This work focuses on a compositional data-driven approach to verify incremental global asymptotic stability (delta-GAS) over interconnected homogeneous networks of degree one with unknown mathematical dynamics. Our proposed approach leverages the concept of incremental input-to-state stability (delta-ISS) of subsystems, characterized by delta-ISS Lyapunov functions. To implement our data-driven scheme, we initially reframe the delta-ISS Lyapunov conditions as a robust optimization program (ROP). Due to the presence of unknown subsystem dynamics in the ROP constraints, we develop a scenario optimization program (SOP) by gathering data from trajectories of each unknown subsystem. However, since the measured one-step transition data are corrupted by noise with a known bound on its norm, rendering the proposed SOP intractable, we introduce an auxiliary SOP that explicitly accommodates noisy measurements. We solve the auxiliary SOP and construct a delta-ISS Lyapunov function for each subsystem with unknown dynamics. We then leverage a small-gain compositional condition to facilitate the construction of an incremental Lyapunov function for an unknown interconnected network based on the data-driven delta-ISS Lyapunov functions of its individual subsystems, while providing correctness guarantees, incorporating the bound on the noise norm. We demonstrate that our data-driven compositional approach reduces the sample complexity to the subsystem level. To validate the effectiveness of our approach, we apply it to an unknown controlled physical nonlinear homogeneous network of degree one, comprising 10000 subsystems. By gathering noisy data from each unknown subsystem, we demonstrate that the interconnected network is delta-GAS with a correctness guarantee.

eess.SY↗

arXiv2026

Compositional Design of Safety Controllers for Large-Scale Stochastic Hybrid Systems

In this work, we propose a compositional scheme based on small-gain reasoning to synthesize safety controllers for interconnected stochastic hybrid systems. In our proposed setting, we first offer an augmented scheme that characterizes each stochastic hybrid subsystem, endowed with both continuous evolution and instantaneous jumps, within a unified framework including both scenarios, implying that its state trajectories coincide with those of the original hybrid subsystem. We then introduce the concept of augmented control sub-barrier certificates (A-CSBCs) for each subsystem, thereby enabling the construction of an augmented control barrier certificate (A-CBC) for an interconnected network (from A-CSBCs of its subsystems) along with its safety controller under small-gain compositional conditions. We eventually leverage the constructed A-CBC to derive a guaranteed lower bound on the safety probability of the interconnected network. While in a monolithic scheme the computational complexity of synthesizing a control barrier certificate via sum-of-squares (SOS) optimization scales polynomially with the overall network size, the proposed compositional framework reduces this dependence to the subsystem size. We illustrate the efficacy of the proposed approach on an interconnected network comprising 1000 stochastic hybrid subsystems with nonlinear dynamics under two distinct interconnection topologies.

eess.SY↗

arXiv2026

Data-Driven Global Stabilization of Unknown Infinite Networks

This paper develops a direct data-driven framework for infinite networks with unknown nonlinear polynomial subsystems, enabling the synthesis of controllers that ensure the entire network is uniformly globally asymptotically stable (UGAS). To address scalability challenges arising from high dimensionality, we develop a data-driven approach to construct an input-to-state stable (ISS) Lyapunov function and its corresponding controller for each unknown subsystem using only a single set of noise-corrupted input-state trajectories collected from that subsystem. Once each subsystem admits a data-driven ISS Lyapunov function, we leverage a compositional small-gain framework for infinite-dimensional spaces to construct a global control Lyapunov function and its associated controller, thereby ensuring UGAS of the entire infinite network. The effectiveness of the proposed data-driven approach is demonstrated through three case studies, including infinite networks of spacecraft, Lorenz chaotic systems, and an academic example with a state-dependent control input matrix.

eess.SY↗

arXiv2026

Towards Certified Sim-to-Real Transfer via Stochastic Simulation-Gap Functions

This paper introduces the notion of stochastic simulation-gap function, which formally quantifies the gap between an approximate mathematical model and a high-fidelity stochastic simulator. Since controllers designed for the mathematical model may fail in practice due to unmodeled gaps, the stochastic simulation-gap function enables the simulator to be interpreted as the nominal model with bounded state- and input-dependent disturbances. We propose a data-driven approach and establish a formal guarantee on the quantification of this gap. Leveraging the stochastic simulation-gap function, we design a controller for the mathematical model that ensures the desired specification is satisfied in the high-fidelity simulator with high confidence, taking a step toward bridging the sim-to-real gap. We demonstrate the effectiveness of the proposed method using a TurtleBot model and a pendulum system in stochastic simulators.

eess.SY↗

arXiv2026

Data-Driven Model Order Reduction of Nonlinear Systems with Noisy Data

Model order reduction techniques simplify high-dimensional dynamical systems by deriving lower-dimensional models that retain essential system characteristics. These techniques are crucial for the controller design of complex systems while significantly reducing computational costs. Nevertheless, constructing effective reduced-order models (ROMs) poses considerable challenges, particularly for nonlinear dynamical systems. These challenges are further exacerbated when the actual system model is unavailable, a scenario frequently encountered in real-world applications. In this work, we propose a data-driven framework for constructing ROMs of nonlinear dynamical systems with unknown mathematical models, enabling controller synthesis directly from the resulting ROMs. We establish similarity relations between the output trajectories of the original systems and those of their ROMs by employing the notion of simulation functions (SFs), thereby enabling a formal characterization of their closeness. To achieve this, we collect one set of noise-corrupted input-state data from the system during a finite-time experiment, upon which we propose conditions to construct both ROMs and SFs simultaneously. These conditions are formulated as data-dependent semidefinite programs. We demonstrate that the data-driven ROMs obtained can be employed to synthesize controllers for the original unknown systems, ensuring that they satisfy high-level logic specifications. This is accomplished by first designing controllers for the data-driven ROMs and then translating the results back to the original systems via interface functions, designed directly from the proposed data-dependent conditions. We evaluate the efficacy of our data-driven framework through two case studies, including a challenging benchmark from the model reduction literature: a circuit of chained inverter gates with 20 state variables.

eess.SY↗

arXiv2026

Data-Driven Control of Large-Scale Networks with Formal Guarantees: A Small-Gain Free Approach

This paper offers a data-driven divide-and-conquer strategy to analyze large-scale interconnected networks, characterized by both unknown mathematical models and interconnection topologies. Our data-driven scheme treats an unknown network as an interconnection of individual agents (a.k.a. subsystems) and aims at constructing their symbolic models, referred to as discrete-domain representations of unknown agents, by collecting data from their trajectories. The primary objective is to synthesize a control strategy that guarantees desired behaviors over an unknown network by employing local controllers, derived from symbolic models of individual agents. To achieve this, we leverage the concept of alternating sub-bisimulation function (ASBF) to capture the closeness between state trajectories of each unknown agent and its data-driven symbolic model. Under a newly developed data-driven compositional condition, we then establish an alternating bisimulation function (ABF) between an unknown network and its symbolic model, based on ASBFs of individual agents, while providing correctness guarantees. Despite the sample complexity in existing work being exponential with respect to the network size, we demonstrate that our divide-and-conquer strategy significantly reduces it to a linear scale with respect to the number of agents. We also showcase that our data-driven compositional condition does not necessitate the traditional small-gain condition, which demands precise knowledge of the interconnection topology for its fulfillment. We apply our data-driven findings to three benchmarks comprising unknown networks with an arbitrary, a-priori undefined number of agents and unknown interconnection topologies.

eess.SY↗

arXiv2026

Safety Controller Synthesis for Stochastic Polynomial Time-Delayed Systems

This work develops a theoretical framework for safety controller synthesis in discrete-time stochastic nonlinear polynomial systems subject to time-invariant delays (dt-SNPS-td). While safety analysis of stochastic systems using control barrier certificates (CBC) has been widely studied, developing safety controllers for stochastic systems with time delays remains largely unexplored. The main challenge arises from the need to account for the influence of delayed components when formulating and enforcing safety conditions. To address this, we employ Krasovskii control barrier certificates, which extend the conventional CBC framework by augmenting it with an additional summation term that captures the influence of delayed states. This formulation integrates both the current and delayed components into a unified barrier structure, enabling safety synthesis for stochastic systems with time delays. The proposed approach synthesizes safety controllers under input constraints, offering probabilistic safety guarantees robust to such delays: it ensures that all trajectories of the dt-SNPS-td remain within the prescribed safe region while fulfilling a quantified probabilistic bound. To achieve this, our method reformulates the safety constraints as a sum-of-squares optimization program, enabling the systematic construction of Krasovskii CBC together with their associated safety controllers. We validate the proposed framework through three case studies, including two physical systems, demonstrating its effectiveness and practical applicability.

eess.SY↗

arXiv2026

A Data-Driven Krasovskii-Based Approach for Safety Controller Design of Time-Delayed Uncertain Polynomial Systems

We develop a data-driven framework for the synthesis of robust Krasovskii control barrier certificates (RK-CBC) and corresponding robust safety controllers (R-SC) for discrete-time input-affine uncertain polynomial systems with unknown dynamics, while explicitly accounting for unknown-but-bounded disturbances and time-invariant delays using only observed input-state data. Although control barrier certificates have been extensively studied for safety analysis of control systems, existing work on unknown systems with time delays, particularly in the presence of disturbances, remains limited. The challenge of safety synthesis for such systems stems from two main factors: first, the system's mathematical model is unavailable; and second, the safety conditions should explicitly incorporate the effects of time delays on system evolution during the synthesis process, while remaining robust to unknown disturbances. To address these challenges, we develop a data-driven framework based on Krasovskii control barrier certificates, extending the classical CBC formulation for delay-free systems to explicitly account for time delays by aggregating delayed components within the barrier construction. The proposed framework relies solely on input-state data collected over a finite time horizon, enabling the direct synthesis of RK-CBC and R-SC from observed trajectories without requiring an explicit system model. The synthesis is cast as a data-driven sum-of-squares (SOS) optimization program, yielding a structured design methodology. As a result, robust safety is guaranteed in the presence of unknown disturbances and time delays over an infinite time horizon. The effectiveness of the proposed method is demonstrated through three case studies, including two physical systems.

eess.SY↗