An Ant Colony Verification Algorithm

Buchi automata are widely used as a modeling formalism in formal verification. The emptiness check procedure is used to carry on the model checking of a model M. of a system, against an LTL formula Phi, that expresses the desidered properties the system should satisfy. Algorithms for the emptiness check on Buchi automata are able to find a faulty computation, if the language accepted by the automaton of the synchronized product of M and Phi is non empty. Nonetheless, these algorithms don´t perform any optimization on such solution. In this paper we propose an ant colony optimization algorithm for the emptiness check of a subclass of Buchi automata, that runs on-the-fly, that is without storing the whole digraph of the automaton in main memory, thus avoiding the problem of exponential growth of the state space. Our approach features a non standard search strategy, with the capability for artificial ants to backtrack during the constructive search, and to modify the graph of the automaton, by removing parts of it when no longer interesting for exploration.