Ant Colony Optimization Based Model Checking Extended by Smell-like Pheromone

Model Checking is a technique to automatically check whether the model representing software or hardware satisfies the given specification. Traditionally, it uses deterministic algorithms, but they consume too many computer resources. To mitigate the problem, the approach based on Ant Colony Optimization (ACO) was proposed. Instead of exhaustively exploring the entire model, the ACO based approach statistically checks a part of the model. Thus the ACO based approach not only suppresses resource consumption, but also guides to reach the goals efficiently. The approach generates shorter counter examples, too. This paper improves the ACO based approach. We further suppresses futile movements of ants while suppressing the resource consumption by introducing smell-like pheromone. ACO detects the semi-shortest path to food by putting pheromones on the trails of ants, but the smell-like pheromone diffuses differently from the traditional pheromone. In our approach, the smell-like pheromone diffuses from foods, guiding ants to the foods, so that our approach not only makes the ants reach the goals farther and more efficiently but also generate much shorter counter examples than those of the traditional approaches do. To demonstrate the effectiveness of our approach, we have implemented our approach on a model checker, and conducted experiments. The experimental results show that our approach is effective for improving execution efficiency and the length of counter examples.