Memory-dependent abstractions of stochastic systems through the lens of transfer operators
Journal:
arXiv
Published Date:
Feb 6, 2025
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.
