Data-driven Construction of Finite Abstractions for Interconnected Systems: A Compositional Approach

TL;DR

The paper tackles scalable verification and controller synthesis for networks of discrete-time control systems with partially unknown dynamics and interconnections. It proposes a data-driven, compositional framework that first constructs finite subsystem abstractions using a data-driven growth bound derived from a growth-bound optimization, and then builds a sparse, decomposed interconnection abstraction via regression, enabling integration into a global symbol-based model. A compositional theory then guarantees a feedback refinement relation between the concrete interconnected system and its composed abstract model, allowing controllers designed for the symbolic model to be refined to the real network. Case studies demonstrate significant scalability gains, effective consensus control under linear interconnections, and stabilization of a high-dimensional tank network, with substantially reduced abstraction sizes and domain sizes for synthesis compared to monolithic approaches.

Abstract

Finite-state abstractions (a.k.a. symbolic models) present a promising avenue for the formal verification and synthesis of controllers in continuous-space control systems. These abstractions provide simplified models that capture the fundamental behaviors of the original systems. However, the creation of such abstractions typically relies on the availability of precise knowledge concerning system dynamics, which might not be available in many real-world applications. In this work, we introduce a novel data-driven and compositional approach for constructing finite abstractions for interconnected systems comprised of discrete-time control subsystems with partially unknown dynamics. These subsystems interact through a partially unknown static interconnection map. Our methodology for abstracting the interconnected system involves constructing abstractions for individual subsystems and incorporating an abstraction of the interconnection map.

Figures (8)

• Figure 1: Interconnection of $N$ finite abstractions $\widehat{\Xi}_i$ while maintaining the feedback refinement relation $Q$. This interconnection is achieved by leveraging the compositionality result (cf. Theorem \ref{['asf_thrm']}).
• Figure 2: A 2-dimensional depiction of a finite abstraction for a subsystem, constructed using Algorithm \ref{['alg_sa']}.
• Figure 3: An illustration of a WDAG with the application of Algorithm \ref{['alg_dec']} where $\sigma=4$.
• Figure 4: The runtime in seconds for systems in \ref{['ex1_f']} and interconnection in \ref{['ex1_w']} are shown for varying $N$. The cumulative runtime is represented by the horizontal bar, segmented into three colors: purple (left) represents abstracting and stacking of the abstraction BDD representations for all subsystems, yellow (middle) denotes the time for approximating the interconnection, and green (right) indicates composing the subsystems and interconnection abstractions.
• Figure 5: The top sub-figure depicts two 8-dimensional trajectories, which are illustrated as two sets of eight scalar-valued trajectories. Each line represents a trajectory $x_i(k)$ for $i\in[1;8]$. Solid lines correspond to a controller enforcing $\Diamond\square\varphi$, while dashed lines represent an inactive controller with $u_i(k)=0$ for all systems $i$ and time steps $k$. Both sets of trajectories initiate from the same initial state $x[0]=[14.8;15.8;15.5;15.1;16.6;18.1;26.5;17.4]$, which lies outside the consensus region $\varphi$ and supports the bimodal property of \ref{['ex2_f']}. The bottom sub-figure depicts the piecewise constant control inputs required to enforce $\Diamond\square\varphi$. The depiction is with slight vertical and horizontal perturbations for visual clarity.

Theorems & Definitions (30)

• Definition 2.1
• Remark 2.2
• Definition 2.3
• Definition 2.4
• Remark 2.5
• Definition 3.1
• Definition 3.2
• Definition 3.3
• Remark 4.1
• Definition 4.2