Data-driven memory-dependent abstractions of dynamical systems via a Cantor-Kantorovich metric

TL;DR

The paper tackles data-driven construction of memory-enhanced abstractions for dynamical systems by introducing a Cantor-Kantorovich metric (CK) between labeled Markov chains. Abstractions are built adaptively from output data, using memory to form nonuniform partitions that ensure safety guarantees. A recursive algorithm CK-rec enables efficient approximation of the CK metric via short-horizon distributions $p_i^k$, and the Refine procedure selects partitions that maximize a CK-based distance. The methodology is demonstrated on a Lorentz-force electron model, where CK-based abstractions yield more accurate safety analyses than conventional grid-based partitions. This work advances data-driven verification and control design by coupling adaptive memory with a scalable optimal-transport-based metric on Markov models.

Abstract

Abstractions of dynamical systems enable their verification and the design of feedback controllers using simpler, usually discrete, models. In this paper, we propose a data-driven abstraction mechanism based on a novel metric between Markov models. Our approach is based purely on observing output labels of the underlying dynamics, thus opening the road for a fully data-driven approach to construct abstractions. Another feature of the proposed approach is the use of memory to better represent the dynamics in a given region of the state space. We show through numerical examples the usefulness of the proposed methodology.

Figures (7)

• Figure 1: Illustration of an adaptive memory abstraction $\Gamma_W$ for a certain dynamical system $\Sigma$ with measure $\lambda$. In this example, $W = \{01_{[0, 1]}, 00_{[0, 1]}, 01_{[-1, 0]}, 11_{[-1, 0]}\}$, as illustrated above. The corresponding abstraction $\Gamma_W$ is given below, with all the possibly non-zero transition probabilities.
• Figure 2: Illustration of the Refine algorithm for a system with $A = \{0, 1\}$. The current model contains three states $W = \left\{01_{[0, 1]}, 00_{[0, 1]}, 1_{[0, 0]}\right\}$. Three sets $W'_1, W'_2, W'_3$ are then constructed, each time expanding one block of the partition into $|A| = 2$ sub-blocks. For each abstraction $\Gamma_{W'_i}$, the distance with the current one is computed: the current model is updated with the model for which the distance is the largest.
• Figure 3: Illustration of the Kantorovich metric linear program \ref{['eq:kant_LP']} for $A = \{0, 1\}$ and $k = 2$. The supplies are given in red, and the demands in blue. To solve this problem, one has to move $\pi^2(00, 11) = 1/4$ supply mass from 00 to 11. To do that, the mass has to travel up to the root. The corresponding Cantor distance is $\mathsf{C}(00, 11) = 2^{0}$. The total cost is therefore $\mathsf{K}_\mathsf{C}(p_1^2, p_2^2) = 1/4$.
• Figure 4: Comparaison of the computational complexity of two methods to solve \ref{['eq:kant_LP']} for $|A| = 2, 3, 4$. In red, the best LP/CO method, and in blue our method as described in Algorithm \ref{['alg:kantorovich']}.
• Figure 5: Illustration of the Lorentz force dynamical system $\Sigma$ as defined in Section \ref{['sec:lorentz_description']}.

Theorems & Definitions (21)

• Remark 1
• Definition 1: Adaptive memory abstraction
• Proposition 1
• proof
• Remark 2
• Definition 2: Kantorovich metric
• Definition 3: Cantor distance
• Lemma 1: See Rozenberg2002
• Definition 4: Cantor-Kantorovich metric
• Remark 3