Model Checking for Rare-Event in Control Logical Petri Nets Based on Importance Sampling

Abstract

In safety-critical system, component failure or dysfunctional component interactions may lead to the occurrence of rare-events, which may cause severe accidents. It is very important to estimate the occurrence probability of rare-events. The extended reachability graph of Control Logical Petri Net (CLPN), which provided a convenient way to express component failure, can be used to verify and estimate the reliability of the safety-critical system with Statistical Model Checking (SMC). However, one of the most important challenges that SMC method faces is the sample size grows too fast while the occurrence probability of rare-events tends to zero. This paper focuses on applying Importance Sampling (IS) on the extended reachability graph of CLPN. By adjusting the state transfer probabilities in the reachability graph, the model checking can be accelerated effectively. The main difficulty in IS is to devise the ideal biasing probability density. In this paper the cross-entropy is used for generating approximately optimal biasing probability density, and we apply an iterative method to accelerate the process. To demonstrate the presented approach, we compare the method based on IS with the traditional SMC method. The results show that the proposed method in this paper accelerates the model checking significantly, at the same time, the results of SMC method serve to validate the results of our approach.

Keywords

• Rare-event simulation
• control logical Petri Net
• statistical model checking
• importance sampling