Model Order Reduction from Data with Certification

TL;DR

The paper tackles the challenge of verifying and synthesizing controllers for high-dimensional dynamical systems when the mathematical model is unknown. It proposes a data-driven MOR framework that fixes a quadratic simulation function, collects two input–state trajectories, and derives a data-based ROM along with an interface map to refine ROM inputs to the original system, providing formal guarantees on trajectory closeness via the SF. The main contributions include sufficient conditions and an SDP-based procedure to construct the ROM and SF from data under a rank condition, along with an interface that enables controller synthesis on the ROM to enforce complex properties (e.g., safety, reach-while-avoid) on the original system. The approach is validated across five benchmarks (motor control, spacecraft docking, blood glucose metabolism, cart system, and a high-dimensional 25-state system), showing accurate ROM–original-system closeness and successful property enforcement, with scalability and a clear path toward nonlinear extensions.

Abstract

Model order reduction (MOR) involves offering low-dimensional models that effectively approximate the behavior of complex high-order systems. Due to potential model complexities and computational costs, designing controllers for high-dimensional systems with complex behaviors can be challenging, rendering MOR a practical alternative to achieve results that closely resemble those of the original complex systems. To construct such effective reduced-order models (ROMs), existing literature generally necessitates precise knowledge of original systems, which is often unavailable in real-world scenarios. This paper introduces a data-driven scheme to construct ROMs of dynamical systems with unknown mathematical models. Our methodology leverages data and establishes similarity relations between output trajectories of unknown systems and their data-driven ROMs via the notion of simulation functions (SFs), capable of formally quantifying their closeness. To achieve this, under a rank condition readily fulfillable using data, we collect only two input-state trajectories from unknown systems to construct both ROMs and SFs, while offering correctness guarantees. We demonstrate that the proposed ROMs derived from data can be leveraged for controller synthesis endeavors while effectively ensuring high-level logic properties over unknown dynamical models. We showcase our data-driven findings across a range of benchmark scenarios involving various unknown physical systems, demonstrating the enforcement of diverse complex properties.

Figures (5)

• Figure 1: (a) Closed-loop trajectories of the original system, starting from $30$ distinct initial conditions, together with (b) the closeness between trajectories of the motor system and those of its corresponding ROM, as well as the mean of errors. As illustrated, all trajectories of the original unknown motor remain within the safe region under the designed ROM controller.
• Figure 2: Trajectories should start from the initial set $X_s$ and reach the target set $X_t$ while avoiding debris in space. As illustrated in (a), trajectories of the spacecraft and its ROM are very close to one another, satisfying the spacecraft's reach-while-avoid property. As shown in (b), the specification is properly fulfilled for $50$ arbitrary trajectories of the spacecraft under the designed ROM controller.
• Figure 3: As the reach-while-avoid specification, trajectories of $x_1$ and $x_2$ should start from the initial set $X_s$ and reach the target set $X_t$ without colliding with the obstacles . As seen, the specification is correctly fulfilled for $20$ arbitrary trajectories of the original system under the designed ROM controller, offering the practicality of our framework for high-dimensional systems.
• Figure 4: The quantified error bound for this example is $0.8609$ according to Theorem \ref{['thm-J19']}. As seen, all plotted errors are below the quantified upper bound $0.8609$, demonstrating the formality of our results.
• Figure 5: The behavior of all states while the reach-while-avoid is solved for the first and second states. As illustrated, there is no anomaly in the behavior of states, and the desired property is clearly satisfied, i.e.,$x_1$ and $x_2$ reached the target .

Theorems & Definitions (16)

• Definition 2.1
• Definition 2.2
• Definition 2.3
• Remark 2.4
• Theorem 2.5
• Remark 2.6
• Remark 2.7
• Remark 3.1
• Lemma 3.2
• proof