Heuristic Genetic Algorithm For Generating Counterexample In Stochastic Model Checking

One of the main advantages of model checking is that it automatically generates counterexamples when the model violates the temporal logic.The counterexample provides basic diagnostic information for system debugging.The debugger can analyze the cause of the system error based on the counterexample and then modify the system.Counterexamples can be a great help in debugging complex systems.Using a dedicate algorithm when generating a counterexample in a stochastic model checking usually consumes too much time and memory,and sometimes can't find a counterexample.To make matters worse,the generation of the smallest counterexamples in stochastic model checking has proven to be an NP-complete problem and is unlikely to be effectively approximated.Although there are some heuristics applied to the generation of counterexamples,it is often difficult to determine heuristics,and the determination of heuristics is critical to the generation of counterexamples.In this paper,we generate a counterexample for stochastic model checking based on a heuristic genetic algorithm.The diagnostic subgraph represents a counterexample and a counterexample is generated by a heuristic genetic algorithm(HGA).The method uses indirect path coding to extend the search range of the state space and uses heuristic operators to generate more efficient paths.The details are as follows:(1)Convert DTMC and MDP into corresponding state transition graphs,and the heuristic genetic algorithm directly searches on the state transition graph;(2)In the process of implementing a heuristic method to extend the genetic algorithm,the indirect path coding scheme and heuristic operator are used,and a suitable fitness function is designed.(3)The HGA generates a counterexample of the reachability property in the DTMC.When the probability of diagnostic subgraph exceeds a given probability threshold,the diagnostic subgraph is a counterexample;(4)Generate a counterexample of the reachability of the MDP through HGA.In order to make the diagnostic path that constitutes the counterexample a valid path under the scheduler,the collection of diagnostic paths is converted to an AND/OR tree,and a counterexample is generated.Finally,case studies are given to illustrate the feasibility and effectiveness of the proposed algorithm.The experimental results show that the HGA algorithm outperforms than the existing counterexample generation algorithm.