Ant Colony Optimization

TLDR

ACO has been successfully applied to combinatorial optimization problems that can be mapped to graph exploration, but existing algorithms struggle with very large graphs that cannot be fully stored in memory. The study introduces a new ACO model that overcomes challenges of huge construction graphs and promotes applying ACO to formal methods in software engineering. The model uses artificial ants that iteratively add graph‑node components, and experiments employ a technique for exploring huge graphs applied to refuting safety properties in concurrent systems. Analysis results clarify the meaning of new parameters and guide selection of suitable parameterization for specific problems.

Abstract

Ant Colony Optimization (ACO) has been successfully applied to those combinatorial optimization problems which can be translated into a graph exploration. Artificial ants build solutions step by step adding solution components that are represented by graph nodes. The existing ACO algorithms are suitable when the graph is not very large (thousands of nodes) but is not useful when the graph size can be a challenge for the computer memory and cannot be completely generated or stored in it. In this paper we study a new ACO model that overcomes the difficulties found when working with a huge construction graph. In addition to the description of the model, we analyze in the experimental section one technique used for dealing with this huge graph exploration. The results of the analysis can help to understand the meaning of the new parameters introduced and to decide which parameterization is more suitable for a given problem. For the experiments we use one real problem with capital importance in Software Engineering: refutation of safety properties in concurrent systems. This way, we foster an innovative research line related to the application of ACO to formal methods in Software Engineering.