The paper proposes a novel model checking algorithm which draws inspiration from the ant collective intelligence. It distributes mobile agents,artificialantsmodeled natural ants,control flow graphs and the state graphs of the programs,the ants can reversely track correct traces and error traces,and deposit two kinds of pheromones which respectively represent correct traces and error traces when traveling between the vertexes of the control flow graphs. According to the pheromones deposited on the traces by ants,we can automatically locate the causes which arouse the specific errors. Furthermore,the ants can work independently and synchronously,so we can track different correct traces and error traces at the same time,and locate the  multiple causes of different errors synchronously. The results of the experiments on medium and small size programs show that the algorithm is effective.