Probabilistic Model Checking By Model Equivalent Reduction And Abstraction

Model checking is a very successful technique to automatically analyze the correctness of a system. Providing counterexample for the refutation of a property is an essential. In order to generate a better counterexample, original model is checked based on equivalent reduction and abstraction.In probabilistic model checking, usually use discrete time Markov chain to represent the model and use a branch of the temporal logic called probabilistic computation tree to represent the properties of the model. In this paper, we propose a new probabilistic model checking algorithm. The model is transformed into new model which only contains a single initial state and the state of a single target against the specific properties of the model. According to the transitive closure of initial state and the reverse transitive closure of target state, reduce the model size. Second, define the concept of the minimal connected components and divide the state space. We detect all the minimal connected components using depth first algorithm. The minimal connected components are represented as discrete time Markov chain with abstraction. The model generates the equivalent acyclic graph after the abstract model of the minimal connected components instead of the original minimal connected components in the original model. In the end, we use the critical subsystems to descript the counterexample, both global search and local search strategy to generate counterexample, the strategy of prevention to avoid new path to prevent repetition, and the algorithm of the operational research to obtain a shortest path between two state.In conclusion, we presented a new framework for the generation of probabilistic counterexamples for discrete time Markov chains based on reduction and abstraction in this paper. Experimental results show that our algorithm greatly simplifies the model size and generate more reasonable counterexamples with least states and paths by means of leader election protocol and the Crowds protocol.