ACOhg: dealing with huge graphs

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.

REFERENCES

• 1: Enrique Alba , José M. Troya, Genetic Algorithms for Protocol Validation, Proceedings of the 4th International Conference on Parallel Problem Solving from Nature, p.870-879, September 22-26, 1996
• 2: Christian Blum , Andrea Roli, Metaheuristics in combinatorial optimization: Overview and conceptual comparison, ACM Computing Surveys (CSUR), v.35 n.3, p.268-308, September 2003 [doi>10.1145/937503.937505]
• 3: E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. The MIT Press, January 2000.
• 4: Janez Demšar, Statistical Comparisons of Classifiers over Multiple Data Sets, The Journal of Machine Learning Research, 7, p.1-30, 12/1/2006
• 5: Marco Dorigo , Thomas Stützle, Ant Colony Optimization, Bradford Book, 2004
• 6: S. Edelkamp, A. Lluch-Lafuente, and S. Leue. Protocol verification with heuristic search. In AAAI-Spring Symposium on Model-based Validation Intelligence, pages 75--83, 2001.
• 7: Stefan Edelkamp , Stefan Leue , Alberto Lluch-Lafuente, Directed explicit-state model checking in the validation of communication protocols, International Journal on Software Tools for Technology Transfer (STTT), v.5 n.2, p.247-267, March 2004 [doi>10.1007/s10009-002-0104-3]
• 8: Patrice Godefroid , Sarfraz Khurshid, Exploring Very Large State Spaces Using Genetic Algorithms, Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, p.266-280, April 08-12, 2002
• 9: G. J. Holzmann. The SPIN Model Checker. Addison-Wesley, 2004.
• 10: G. Leguizamón and Z. Michalewicz. A new version of Ant System for subset problems. In P. A. et al., editor, Proc. of the 1999 Congress on Evolutionary Computation, pages 1459--1464, Piscataway, New Jersey, USA, 1999. IEEE Computer Society Press.
• 11: A. Lluch-Lafuente. Symmetry reduction and heuristic search for error detection in model checking. In Workshop on Model Checking and Artificial Intelligence, August 2003.
• 12: Zohar Manna , Amir Pnueli, The temporal logic of reactive and concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1992

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.8 Problem Solving, Control Methods, and Search
          Subjects: Heuristic methods

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Model checking

  G. Mathematics of Computing
  G.1 NUMERICAL ANALYSIS
      G.1.6 Optimization
          Subjects: Global optimization

General Terms:
Algorithms, Experimentation, Verification

Keywords:
SPIN, ant colony optimization, metaheuristics