An Ant Colony Verification Algorithm
R.achid Rebiha, Giovanni Luca Ciampaglia · Seventh International Conference on Intelligent Systems Design and Applications (ISDA 2007) · 2007
B¨uchi automata are widely used as a modeling formal- ism 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 , that expresses the desidered properties the system should satisfy. Algorithms for the emptiness check on B¨uchi automata are able to find a faulty computation, if the language accepted by the au- tomaton of the synchronized product of M and is non empty. Nonetheless, these algorithms don't perform any op- timization on such solution. In this paper we propose an ant colony optimization algorithm for the emptiness check of a subclass of B¨uchi 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.