Robustly Complete Finite-State Abstractions for Verification of Stochastic Systems

In this paper, we focus on discrete-time stochastic systems modelled by nonlinear stochastic difference equations and propose robust abstractions for verifying probabilistic linear temporal specifications. The current literature focuses on developing sound abstraction techniques for stochastic dynamics without perturbations. However, soundness thus far has only been shown for preserving the satisfaction probability of certain types of temporal-logic specification. We present constructive finite-state abstractions for verifying probabilistic satisfaction of general {\omega}-regular linear-time properties of more general nonlinear stochastic systems. Instead of imposing stability assumptions, we analyze the probabilistic properties from the topological view of metrizable space of probability measures. Such abstractions are both sound and approximately complete. That is, given a concrete discrete-time stochastic system and an arbitrarily small L1-perturbation of this system, there exists a family of finite-state Markov chains whose set of satisfaction probabilities contains that of the original system and meanwhile is contained by that of the slightly perturbed system. A direct consequence is that, given a probabilistic linear-time specification, initializing within the winning/losing region of the abstraction system can guarantee a satisfaction/dissatisfaction for the original system. We make an interesting observation that, unlike the deterministic case, point-mass (Dirac) perturbations cannot fulfill the purpose of robust completeness.