Abstract:Statistical model checking (SMC) is an important method for the verification of safety of stochastic hybrid system (SHS), while for the system with extremely high safety requirements, the unsafe events and the failures of the system are rare events. In this case, it is difficult for SMC to draw the samples satisfying the rare properties and the SMC becomes infeasible. To solve this problem, an SMC method based on cross entropy iterative learning is proposed in this study. First, a continuous time Markov chain (CTMC) is used to represent the path probability space of the SHS, and based on the path space, a parameterized probability distribution family is derived. Then, the cross-entropy optimization model on the path space is constructed and an iterative learning algorithm is proposed, which can find the optimal importance distribution in the path space. Finally, an algorithm for verification of rare properties is given. Experimental results show that the proposed method can effectively verify rare properties of the SHS, and compared with some heuristic importance sampling methods, in the same number of samples, the estimated value of the proposed method can be better distributed near the sample mean, and the standard deviation and relative error are reduced by more than an order of magnitude.