面向基本蟻群算法的形式化研究.pdf

1、近年來，人工智能領(lǐng)域飛速發(fā)展，仿生優(yōu)化算法是其中的一個(gè)重要方向。蟻群算法(ant colony algorithm)又稱為螞蟻算法就是通過模擬蟻群覓食行為而發(fā)展起來的一類仿生優(yōu)化算法，且已廣泛應(yīng)用于路徑規(guī)劃、網(wǎng)絡(luò)路由等多個(gè)領(lǐng)域。然而蟻群算法存在著基礎(chǔ)理論研究不夠完善、研究相對滯后，缺乏新的分析和建模工具的問題。本文從以上問題出發(fā)，將形式化方法用于對蟻群算法的研究中，主要完成了以下工作:
　　首先對形式化方法進(jìn)行了深入的分析研究，對

2、三種常用的形式化驗(yàn)證方法進(jìn)行了詳細(xì)的分析與對比，最終將定理證明方法確定為本文的形式化驗(yàn)證方法。
　　接著對基本蟻群算法的原理進(jìn)行了詳細(xì)的闡述，然后從算法的實(shí)現(xiàn)出發(fā)對其進(jìn)行了形式化分析與建模，用層次化的形式化建模方法自外向內(nèi)進(jìn)行分析，然后自內(nèi)向外進(jìn)行形式化建模，將基本蟻群算法分為了三層，在高階邏輯定理證明器中構(gòu)建了一個(gè)可擴(kuò)展的基本蟻群算法形式化模型，并完成了它的形式化描述。
　　選擇正反饋性和自組織性作為本文的驗(yàn)證目標(biāo)。首先對

3、這兩個(gè)性質(zhì)規(guī)范進(jìn)行形式化描述，然后通過對比詳細(xì)闡述了兩種驗(yàn)證方法:正向證明和目標(biāo)制導(dǎo)法，最后通過之前構(gòu)建的基本蟻群算法形式化模型，選用目標(biāo)制法，在高階邏輯定理證明器HOL4中完成了規(guī)范的形式化驗(yàn)證，證明了此建模方法的有效性。
　　最后將已建立的基本蟻群算法形式化模型用于對一個(gè)優(yōu)化蟻群算法形式化建模，進(jìn)一步論證了此模型的有效性與本工作的意義。
　　對蟻群算法進(jìn)行形式化研究，不僅為算法的基礎(chǔ)理論研究提供了新方法，也可以作為算法應(yīng)