Reach-avoid Analysis for Stochastic Discrete-time Systems
Xue Bai, Renjue Li, Naijun Zhan, Martin Fränzle
Abstract
Stochastic discrete-time systems, i.e., discrete-time dynamic systems subject to stochastic disturbances, are an essential modelling tool for many engineering systems, and reach-avoid analysis is able to guarantee safety (i.e., via avoiding unsafe sets) and progress (i.e., via reaching target sets). In this paper we study the reach-avoid problem of stochastic discrete-time systems over open (i.e., not bounded a priori) time horizons. The stochastic discrete-time system of interest is modeled by iterative polynomial maps with stochastic disturbances, and the problem addressed is to effectively compute an inner approximation of its p-reach-avoid set. The p-reach-avoid set collects those initial states that give rise to a bundle of trajectories which with probability being larger than p eventually hits a designated set of target states while remaining inside a set of safe states before the first hit. The computation of the p-reach-avoid set is first reduced to the computation of a corresponding strict p-super-level set and is then inner-approximated by solving a semi-definite programming problem obtained from a relaxation of the definition of the super-level set. Two examples demonstrate the proposed approach.