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

Published in *American Control Conference (ACC)*, 2020

Recommended citation: M. Dutreix, C. Santoyo, M. Abate, S. Coogan. "Interval-valued Markov Chain Abstraction of Stochastic Systems using Barrier Functions" * American Control Conference (ACC), to appear *.

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.