Interval-valued Markov Chain Abstraction of Stochastic Systems using Barrier Functions

This paper presents a stochastic barrier function-based abstraction technique for discrete-time stochastic systems.Recent works have shown the potential of Interval-valued Markov Chain abstractions for conducting efficient verification of continuous-state, discrete-time stochastic systems against complex objectives, as well as efficient synthesis for finite-mode switched stochastic systems. Such Markovian abstractions allow for a range of transition probabilities between its states. In this work, we address the problem of constructing Interval-valued Markov Chain abstractions for polynomial systems using stochastic barrier functions. Stochastic barrier functions serve as Lyapunov-like probabilistic certificates of forward set invariance. Specifically, given a finite partition of the system’s domain, we show that bounds on the probability of transition between any two elements of the partition are found by generating stochastic barrier functions via optimization procedures in the form of Sum-of-Squares programs. We present an algorithm for solving these optimization problems whose implementation is demonstrated in a verification and a synthesis case study.

Use Google Scholar for full citation. Download paper here