Safety Verification Of Stochastic Hybrid Systems Based On Semidefinite Programming

Stochastic hybrid systems are complicated dynamic systems that are governed by interacting discrete,continuous and stochastic dynamics.As a common mathematical model for cyber-physical systems,stochastic hybrid systems are widely used in safetycritical areas like energy,medical,traffic and national defense.Therefore the study of safety verification problem of stochastic hybrid sytems is of great significance both in theory and in practice.Since sotchastic systems can be viewed as the combination of serveral stochastic continuous systems,the study on safety verification of stochastic continuous systems has great theoretic value.The dissertation presents a safety verification method for stochastic continuous systems based on stochastic barrier cerificate and a tool to verify the safety of continuous systems according to the proposed method.The main work is carried out as follows:· We study the safety verification of a class of stochastic continuous sytems equipped with both random initial states and stochastic differential equations.Firstly,the method to select suitable initial state set is applied and the safety verification problem is converted into the study of stochastic continuous systems equipped with deterministic initial state.Secondly,the upper bound of the probability of the trajectory entering the unsafe region is computed by using stochastic barrier cerificates.By combining these two methods,we obtain the lower bound of safety probability of stochastic continuous systems.· We propose a new algorithm for safety verification of stochastic continuous systems based on semidefinite programming and sums of squares relaxation.which can be seperated into the following two parts.Firstly,we construct the parameterize initial state set according to the probability density function of the initial distribution and compute the probability of the initial state falling into the initial state set.Secondly,we solve the semidefinite programming converted from the stochastic barrier certificate model.Since semidefinite programmings can be solved efficiently by applying the interior point method,the proposed method has polynomial time complexity.· We develop a continuous systems safety verification tool SCSVer based on the algorithm proposed in the paper,combine with existing research results in related fields and the open source software package Se Du Mi and SOSTOOLS,which can be used for safety verification of semi-algebraic deterministic continuous sytems and semi-algebraic stochastic continuous systems.In summary,we firstly convert the safety verification problem of given semialgebraic stochastic continuous systems into the safety verification of stochastic continuous systems with deterministic initial state set,then we solve the lower bound of safety probability by stochastic barrier ceritificate.According to the process,we develop a tool SCSVer which can be used to verify the safety problem of various kinds of semi-algebraic deterministic and stochastic continuous systems.