Memory-dependent abstractions of stochastic systems through the lens of transfer operators

TL;DR

This work tackles formal verification of stochastic systems under uncertainty by introducing memory-dependent abstractions that capture non-Markovian effects arising from discretization. It builds an $\ell$-memory abstraction via lifting the state to an $\ell$-long sequence and applying Galerkin approximations to the lifted transfer operator, producing a finite Markov model with provable total-variation guarantees. The key contributions are a formalism for these abstractions based on transfer operators, a computable upper bound on $\mathsf{TV}$ between the true and approximated state distributions, and numerical evidence that increasing memory improves approximation quality in both partially observed and fully discretized scenarios. This approach enables safer, more accurate verification and control design for complex stochastic systems by explicitly accounting for memory effects introduced by abstraction.

Abstract

With the increasing ubiquity of safety-critical autonomous systems operating in uncertain environments, there is a need for mathematical methods for formal verification of stochastic models. Towards formally verifying properties of stochastic systems, methods based on discrete, finite Markov approximations -- abstractions -- thereof have surged in recent years. These are found in contexts where: either a) one only has partial, discrete observations of the underlying continuous stochastic process, or b) the original system is too complex to analyze, so one partitions the continuous state-space of the original system to construct a handleable, finite-state model thereof. In both cases, the abstraction is an approximation of the discrete stochastic process that arises precisely from the discretization of the underlying continuous process. The fact that the abstraction is Markov and the discrete process is not (even though the original one is) leads to approximation errors. Towards accounting for non-Markovianity, we introduce memory-dependent abstractions for stochastic systems, capturing dynamics with memory effects. Our contribution is twofold. First, we provide a formalism for memory-dependent abstractions based on transfer operators. Second, we quantify the approximation error by upper bounding the total variation distance between the true continuous state distribution and its discrete approximation.

Figures (5)

• Figure 1: Loss of the Markov property. Consider a stochastic system defined by $x_{k+1} = x_k + \pi/2 + w_k \pmod{2\pi}$, where $w_k$ is a noise whose support is $[0, \pi/10]$. While the original system is Markovian, the discrete process tracking only in which region $x_k$ lies is not. Specifically, one can see that a state $x_{k}$ can jump from $A_2$ to $A_1$ with non-zero probability, i.e. $\mathbb{P}[x_{k+1} \in A_1 | x_{k} \in A_2] > 0$. However, when a larger memory is considered, we see that, if this state was initially in $A_1$, it cannot jump successively to $A_2$ and back to $A_1$, i.e. $\mathbb{P}[x_{k+2} \in A_1 | x_{k+1} \in A_2, x_k \in A_1] = 0$. The Markov property is therefore lost, since $\mathbb{P}[x_{k+1} \in A_1 | x_{k} \in A_2] \neq \mathbb{P}[x_{k+2} \in A_1 | x_{k+1} \in A_2, x_k \in A_1]$.
• Figure 2: Domino rule for memory-dependent abstractions. Let $A_1$ and $A_2$ be two blocks of an initial partition on the state space $E$. $A_1$ and $A_2$ correspond to states of a 1-memory (memoryless) abstraction. Towards a 2-memory abstraction for deterministic systems, the domino rule proceeds as follows. The cell $A_1$ is divided into $A_1, A_1$ and $A_1, A_2$, the sets of states that are in $A_1$ and that will respectively be either in $A_1$ or in $A_2$ at the next timestep (the same happens to subdivide $A_2$). For stochastic systems, such division is not possible, as generally, even though the system might be in a specific state in $A_1$, it can visit any of $A_1$ or $A_2$ in the next step, due to stochasticity; in other words, there is no set of states in $A_1$ that deterministically visit either of $A_1$ and $A_2$ in the next step (similarly for the states initially in $A_2$).
• Figure 3: Summary of the method described in Algorithm \ref{['alg:l-approx']}, from left to right. Step a) We consider the lifted process defined in \ref{['eq:system_lift']}. Step b) We project the $x_0$-to-$x_{\ell-1}$ joint distribution on a finitely generated space $D_n^\ell$. Step c) We propagate it with the Galerkin approximation $P_\ell$ to get the approximate $x_{k-\ell+1}$-to-$x_k$ joint distribution. Step d) We marginalize it to retrieve the approximate density at $x_k$.
• Figure 4: Approximation quality of $\ell$-memory Markov models for partially observable systems. Introducing memory improves approximation quality.
• Figure 5: Approximation quality of memory-dependent abstractions of an observable system. One can see that, for the same number of transition probabilities ($n^{\ell+1} = 531441$ in both cases), starting from a coarser partition and increasing the memory leads to better approximations.

Theorems & Definitions (21)

• Definition 1: Invariant measure
• Remark 1
• Definition 2: $\mu$-weighted probability density function Prinz2011
• Remark 2
• Remark 3
• Definition 3: Transfer operator
• Definition 4: Transfer operator spectrum
• Definition 5: Projection operator
• Remark 4
• Remark 5: Notations