Ant Colony Optimization for Model Checking

Abstract Model Checking is a well-known and fully automatic technique for checking software properties, usually given as temporal logic formulas on the program variables. Most of model checkers found in the literature use exact deterministic algorithms to check the properties. These algorithms usually require huge amounts of computational resources if the checked model is large. We propose here the use of Ant Colony Optimization (ACO) to check safety properties of concurrent systems. ACO algorithms are stochastic techniques belonging to the class of metaheuristic algorithms [1] and inspired in the foraging behavior of the real ants. The main idea consists in using artificial ants which simulate this behavior in a graph. Artificial ants are placed on initial nodes of the graph and they jump stochastically from one node to another in order to search the shortest path from the initial node to an objective one. The cooperation among the artificial ants is a key factor in the search. This c...

• Type: Conference
• Year: 2007
• Where: EUROCAST
• Authors: Enrique Alba, J. Francisco Chicano
• Keywords: ACO Algorithm, Artificial Ants, EUROCAST 2007, Hardware, Real Ants