Probabilistic Safety Verification of Stochastic Hybrid Systems Using Probably Approximately Correct Barrier Certificates

The probabilistic safety verification problem of stochastic hybrid systems is very important. In this paper, for a given stochastic hybrid system, an algorithm for generating probabilistic barrier certificates is proposed to verify the safety of the system. By solving the mixed integer programming model, the solution of probabilistic barrier certificate is transformed into an optimization problem. This paper implements the probabilistic barrier certificate generation tool PBC and evaluates its performance on three benchmark systems. Experimental results show that compared with the existing methods PBCG, PBC can verify the safety of the system with a higher success probability.