蚁群智能模型检测算法借鉴了自然界中蚂蚁通过信息素相互沟通，从而完成觅食、搬迁等需要协作的复杂社会活动的原理。通过分布在程序控制流图和状态图上的代理，即人工蚂蚁的回溯来跟踪寻找模型中的正确路径和错误路径，人工蚂蚁在控制流图上移动时，分别在正确路径和错误路径上释放两种不同的信息素，通过对两种信息素的对比，可自动定位出程序中引发特定错误的原因。由于人工蚂蚁之间相互独立、并行工作，因此算法能够同时、并行地跟踪多条正确路径和错误路径，也可同时定位出引发多个不同错误的不同原因。通过对中小规模程序的检测，结果表明，该算法是有效的。

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.