Formalization Of Basic Ant Colony Algorithm

In recent years,the field of artificial intelligence is developing rapidly,bionic optimization algorithm is one of the important direction.Ant colony algorithm,is a kind of bionic optimization algorithm which has been developed by simulating ant colony foraging behavior,and has been widely used in many fields such as path planning and network routing.However,there are still some defects in the ant colony algorithm that the basic theory research is not perfect,which is lagging behind the application research and lack of new analysis and modeling tools.In this paper,from the above problems,the formal method is used in research of ant colony algorithm,mainly completed the following work:Firstly,the formal method is analyzed and studied in detail.Three kinds of formal verification methods are analyzed and compared in detail.Finally,the theorem proving method is defined as the formal verification method.Then,the principle of basic ant colony algorithm is expounded in detail,and then the formal analysis and modeling are carried out from the realization of the algorithm.The algorithm is analyzed from the outside to the inside,and then from the inside to outside for the formal modeling,the basic ant colony algorithm is divided into three layers.A formal model of scalable basic ant colony algorithm is constructed in high-order logic theorem proving,and its formal description is completed.Select positive feedback and self-organization as the validation goal of this paper.Firstly,the formal description of these two natures is described,and then two kinds of verification methods are described in detail:the positive proof and the target guidance method.Finally,by using the the foemal model of the basic ant colony algorithm and the target method,the formal verification of the norm is proved in the high order logic theorem HOL4,which proves the validity of the modeling method.Finally,the formal model of the basic ant colony algorithm is used to formalize the modeling of an optimized ant colony algorithm,The validity of the model and the significance of this work are further demonstrated.Formal research on ant colony algorithm not only provides a new method for the basic theory research of the algorithm,but also can be used as the basis for the wider application of the algorithm.In addition,the formal method is used in the ant colony algorithm to broaden the application field of the formal method itself,and it has practical significance to improve the automation level of the theorem proving method.