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 305
- Downloads 0
Inpainting large missing regions based on Seam Carving
Inpainting techniques are developed to recover missing image information. Existing inpainting approaches are: Partial Differential Equations Based Inpainting (PDE-BI) and Exemplar-Based Inpainting (EBI). PDE-BI methods u...
Stochastic-Based Power Consumption Analysis for Data Transmission in Wireless Sensor Networks
Wireless sensor networks (WSNs) provide a lot of emerging applications. They suffer from some limitations such as energy constraints and cooperative demands essential to perform sensing or data routing. The networks coul...
Parallel Simulation of Queueing Petri Nets
Queueing Petri Nets (QPNs) are a powerful formalism to model the performance of software systems. Such models can be solved using analytical or simulation techniques. Analytical techniques suffer from scalability issues,...
Map Matching Algorithm: Trajectory and Sequential Map Analysis on Road Network
The Global Positioning System (GPS) tracking data is essential for sensor data sources. It plays an important role for various systems like Traffic assessment and Prediction, routing and navigation, Fleet management etc. T...
Information seeking behaviour and purchasing decision: case study in digital cameras
This case study explores the information seeking behaviour of digital camera consumers based on Assael’s consumer information acquisition and processing model. 135 responses were received from potential target group who...