Safety Analysis of Linear Discrete-time Stochastic Systems: Work-in-Progress

We study the problem of safety verification of linear discrete-time stochastic systems (linear DTSS) over bounded and unbounded time horizons. Linear DTSS capture random processes, where the one-step transition relation between the current random vector X and the next-step random vector X' is linear and is given by X' = AX + W, where A is an n x n matrix and W is a random noise vector. We assume that the initial and noise random vectors are multivariate normal. Our safety problem consists of checking whether a random vector in the unsafe set is reachable from a random vector in the initial set through a random process of the linear DTSS in either a given bounded or unbounded number of steps. For bounded safety verification, we reduce the problem to the satisfiability of a semidefinite programming problem. For the unbounded safety verification, we propose a novel abstraction procedure to reduce the safety problem to that of a finite graph, wherein, the nodes of the graph correspond to the regions of a partition of the random vector space, in contrast to existing works that partition the state-space. More precisely, we partition the parameter space of normal random vectors, namely, the space of means and covariance matrices, and apply semi-definite programming to compute the edges. We show that our abstraction procedure is sound.