inis 16(7): e1

Research Article

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

Download929 downloads
  • @ARTICLE{10.4108/eai.21-4-2016.151156,
        author={Tsutomu Kumazawa and Chihiro Yokoyama and Munehiro Takimoto and Yasushi Kambayashi},
        title={Ant Colony Optimization Based Model Checking Extended by Smell-like Pheromone},
        journal={EAI Endorsed Transactions on Industrial Networks and Intelligent Systems},
        keywords={Ant Colony Optimization, Model Checking, State Explosion},
  • Tsutomu Kumazawa
    Chihiro Yokoyama
    Munehiro Takimoto
    Yasushi Kambayashi
    Year: 2016
    Ant Colony Optimization Based Model Checking Extended by Smell-like Pheromone
    DOI: 10.4108/eai.21-4-2016.151156
Tsutomu Kumazawa1,*, Chihiro Yokoyama2, Munehiro Takimoto2, Yasushi Kambayashi3
  • 1: Software Research Associates, Inc, 2-32-8 Minami-Ikebukuro, Toshima-ku, Tokyo 171-8513, Japan
  • 2: Tokyo University of Science, 2641 Yamazaki, Noda-shi, Chiba 278-8510, Japan
  • 3: Nippon Institute of Technology, 4-1 Gakuendai, Miyashiro-machi, Minamisaitama-gun, Saitama 345-8501, Japan
*Contact email:


Model Checking is a technique for automatically checking the model representing software or hardware about whether they satisfy the corresponding specifications. Traditionally, the model checking uses deterministic algorithms, but the deterministic algorithms have a fatal problem. They are consuming too many computer resources. In order to mitigate the problem, an approach based on the Ant Colony Optimization (ACO) was proposed. Instead of performing exhaustive checks on the entire model, the ACO based approach statistically checks a part of the model through movements of ants (ant-like software agents). Thus the ACO based approach not only suppresses resource consumption, but also guides the ants to reach the goals efficiently. The ACO based approach is known to generate shorter counter examples too. This article presents an improvement of the ACO based approach. We employ a technique that further suppresses futile movements of ants while suppressing the resource consumption by introducing a smell-like pheromone. While ACO detects the semi-shortest path to food by putting pheromones on the trails of ants, the smell-like pheromone diffuses differently from the traditional pheromone. In our approach, the smell-like pheromone diffuses from food, and guidesants to the food. Thus our approach not only makes the ants reach the goals farther and more efficiently but also generates much shorter counter examples than those of the traditional approaches. In order to demonstrate the effectiveness of our approach, we have implemented our approach on a practical model checker, and conducted numerical experiments. The experimental results show that our approach is effective for improving execution efficiency and the length of counter examples.