Ant Colony Optimization Based Model Checking Extended by Smell-like Pheromone
Journal Title: EAI Endorsed Transactions on Industrial Networks and Intelligent Systems - Year 2016, Vol 3, Issue 7
Abstract
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.
Authors and Affiliations
Tsutomu Kumazawa, Chihiro Yokoyama, Munehiro Takimoto, Yasushi Kambayashi
Keywords
Related Articles
- EP ID EP46042
- DOI http://dx.doi.org/10.4108/eai.21-4-2016.151156
- Views 274
- Downloads 0
Cooperative Non-Orthogonal Multiple Access for Future Wireless Communications
There is a huge demand for increased connectivity and reliability of devices in the fifth generation and beyond of wireless communications so as to ensure massive connectivity and high spectral efficiency. Recently, power d...
Attribution of Cyber Attacks on Industrial Control Systems
In order to deter or prosecute for cyber attacks on industrial control systems it is necessary to assign attribution to the attacker and define the type of attack so that international law enforcement agencies or nationa...
Constructing a Knowledge Base for Entertainment by Interlinking Multiple Data Sources
This paper describes a knowledge base for entertainment domains, including movies, music, and celebrities. We present an ontology model for representing graph-based knowledge, and describe knowledge processing techniques...
Hybrid Simulation Using SAHISim Framework
Hybrid systems such as Cyber Physical Systems (CPS) are becoming more important with time. Apart from CPS there are many hybrid systems in nature. To perform a simulation based analysis of a hybrid system, a simulation f...
Merging OMG Standards in a General Modeling, Transformation, and Simulation Framework
Test-driven Agile Simulation (TAS) is a general-purpose approach that combines model-driven engineering, simulation, and testing techniques to improve overall quality for the development process. TAS focuses on the const...