Ant Colony Optimization (ACO) has been successfully ap- plied 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 algo- rithms are suitable when the graph is not very large (thou- sands of nodes) but is not useful when the graph size can be a challenge for the computer memory and cannot be com- pletely 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 under- stand 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 fos- ter an innovative research line related to the application of ACO to formal methods in Software Engineering.