本文主要內(nèi)容正是基于M．A．GutierrezNaranjo和D．RamirezMartinez開(kāi)發(fā)的Snps-GUI_v1．1來(lái)實(shí)現(xiàn)脈沖神經(jīng)膜系統(tǒng)計(jì)算模型形式化驗(yàn)證的仿真并通過(guò)分析自動(dòng)生成的格局(組態(tài))轉(zhuǎn)移圖，找尋轉(zhuǎn)移圖與脈沖神經(jīng)膜系統(tǒng)之間的相關(guān)性并總結(jié)出一般性結(jié)論，達(dá)到了通過(guò)計(jì)算機(jī)輔助驗(yàn)證脈沖神經(jīng)膜系統(tǒng)正確性與完整性的目的．結(jié)論顯示，轉(zhuǎn)移圖能有效解決脈沖神經(jīng)膜系統(tǒng)形式化驗(yàn)證困難的問(wèn)題，是形式化驗(yàn)證的有效方法之一，也能幫助我們正確理解脈沖神經(jīng)膜系統(tǒng)的計(jì)算過(guò)程，進(jìn)一步設(shè)計(jì)及改進(jìn)系統(tǒng)，從而減輕了繁重的腦力計(jì)算;而SnpsGUI_v1．1仿真軟件能自動(dòng)生成系統(tǒng)格局轉(zhuǎn)移圖，使我們擺脫了繁瑣的手工繪制，是研究人員有力的輔助工具．本文內(nèi)容安排如下:第2節(jié)介紹了脈沖神經(jīng)膜系統(tǒng)的定義及相關(guān)概念;第3節(jié)分別實(shí)現(xiàn)了一個(gè)產(chǎn)生無(wú)限數(shù)集和一個(gè)產(chǎn)生語(yǔ)言的脈沖神經(jīng)膜系統(tǒng)的形式化驗(yàn)證的仿真，分析了轉(zhuǎn)移圖與計(jì)算模型之間的關(guān)系并歸納出3個(gè)一般性結(jié)論;最后總結(jié)了本文的主要結(jié)論，對(duì)其它更有效的形式化驗(yàn)證方法提出了展望，并對(duì)SnpsGUI_v1．1仿真軟件進(jìn)行了評(píng)述，提出了改進(jìn)方向．

脈沖神經(jīng)膜系統(tǒng)的定義及相關(guān)概念

一個(gè)度數(shù)為m(m≥1)的脈沖神經(jīng)膜系統(tǒng)形式化定義［8］如下:∏=(O，σ1，σ2，…，σm，syn，in，out)，其中:1)O={a}為一個(gè)單字母集合，a表示單脈沖;2)σ1，σ2，…，σm表示系統(tǒng)∏中包含有m個(gè)形如σi=(ni，Ri)，1≤i≤m的神經(jīng)元，其中:(1)ni≥0表示神經(jīng)元σi在初始狀態(tài)時(shí)包含的脈沖個(gè)數(shù)，(2)Ri表示神經(jīng)元σi中的所有規(guī)則的有限集合，規(guī)則的形式有如下兩種:①E/ac→ap;d，E為a的正則表達(dá)式，其中c≥1，d≥0，p≥1，且c≥p;②E'/as→λ，E'為a的正則表達(dá)式，s≥1，且對(duì)于規(guī)則Ri中形式為①的每條規(guī)則E/ac→ap;d，滿足L(E)∩L(E')=?;3)syn?{1，2，…，m}×{1，2，…，m}表示所有神經(jīng)元之間的連接關(guān)系，對(duì)任意1≤i≤m，有(i，i)?syn;4)in，out∈{1，2，…，m}分別表示輸入神經(jīng)元和輸出神經(jīng)元．形式①、②的規(guī)則分別稱為廣義激發(fā)、廣義遺忘規(guī)則．若①型規(guī)則滿足p=1、②型規(guī)則滿足E=as，則分別稱為標(biāo)準(zhǔn)激發(fā)規(guī)則和標(biāo)準(zhǔn)遺忘規(guī)則．激發(fā)規(guī)則E/ac→ap;d滿足E=ac時(shí)，則把它寫(xiě)為ac→ap;d;同時(shí)若滿足d=0，則進(jìn)一步簡(jiǎn)寫(xiě)為E/ac→ap．類(lèi)似地，遺忘規(guī)則E'/as→λ滿足E'=as時(shí)，則可以簡(jiǎn)寫(xiě)為as→λ．激發(fā)規(guī)則的使用:在某一時(shí)刻，若神經(jīng)元σi中包含k個(gè)脈沖，且aK∈L(E)及k≥c，則神經(jīng)元σi可以使用激發(fā)規(guī)則E/ac→ap;d．當(dāng)使用此規(guī)則后，神經(jīng)元σi將消耗c個(gè)脈沖;同時(shí)，經(jīng)過(guò)d個(gè)單位時(shí)間后將產(chǎn)生p個(gè)新脈沖，且立即向與之下連的所有相鄰神經(jīng)元分別發(fā)送p個(gè)脈沖．在使用該規(guī)則到發(fā)送新脈沖的d個(gè)單位時(shí)間內(nèi)，該神經(jīng)元處于關(guān)閉狀態(tài)．假如神經(jīng)元σi在第t步使用了激發(fā)規(guī)則E/ac→ap;d，d≥1，則此神經(jīng)元在第t步到第t+d－1步是關(guān)閉的．當(dāng)一個(gè)神經(jīng)元處于關(guān)閉狀態(tài)時(shí)，則其中的任何規(guī)則都不能使用且不能接收新脈沖;只要狀態(tài)變?yōu)殚_(kāi)放后，才可以使用規(guī)則和接收新脈沖．遺忘規(guī)則的使用:在某一時(shí)刻，若神經(jīng)元σi包含了k'個(gè)脈沖，且滿足ak'∈L(E')和k'≥S，則神經(jīng)元σi使用遺忘規(guī)則E'＇as→λ，即消耗掉s個(gè)脈沖，且不產(chǎn)生新脈沖．在一個(gè)神經(jīng)元中可能存在多條激發(fā)規(guī)則同時(shí)滿足的情形，如存在兩條激發(fā)規(guī)則E1/ac1→ap1;d1和E2/ac2→ap2;d2滿足條件L(E1)∩L(E2)≠?．某時(shí)刻若出現(xiàn)這種神經(jīng)元σi中有多條激發(fā)規(guī)則可以使用時(shí)，此神經(jīng)元能且只能隨機(jī)地選擇其中一條規(guī)則使用，這就是規(guī)則使用的不確定性．上述的脈沖神經(jīng)膜系統(tǒng)∏在某時(shí)刻的格局定義為CK=(r1/t1，r2/t2，…，rm/tm)，1≤i≤m，其中ri表示神經(jīng)元σi在此時(shí)刻包含的脈沖個(gè)數(shù)，ti表示神經(jīng)元σi由關(guān)閉狀態(tài)轉(zhuǎn)變?yōu)殚_(kāi)放狀態(tài)需要的步數(shù)．系統(tǒng)∏的初始格局可以表示為C0=(r1/0，r2/0，…，rm/0)，格局C1到格局C2的轉(zhuǎn)移表示為C1?C2．任意由初始格局開(kāi)始的一系列的格局轉(zhuǎn)移被稱之為系統(tǒng)∏的一個(gè)計(jì)算，系統(tǒng)中的所有神經(jīng)元都處于開(kāi)放狀態(tài)，但無(wú)規(guī)則可用的格局稱為終止格局，能到達(dá)終止格局的計(jì)算稱為可終止的計(jì)算．

脈沖神經(jīng)膜系統(tǒng)形式化驗(yàn)證仿真與分析

1.脈沖神經(jīng)膜系統(tǒng)形式化驗(yàn)證仿真實(shí)現(xiàn)引言中提到的SnpsGUI_v1．1軟件是迄今唯一的一款基于脈沖神經(jīng)膜系統(tǒng)的仿真工具，它能接受脈沖神經(jīng)膜系統(tǒng)的描述并自動(dòng)逐步輸出系統(tǒng)的格局轉(zhuǎn)移圖．該軟件具有模塊化、靈活性、界面友好等特點(diǎn)，適用于研究人員理解脈沖神經(jīng)膜系統(tǒng)的計(jì)算過(guò)程，形式化驗(yàn)證脈沖神經(jīng)膜系統(tǒng)的正確性和完整性，進(jìn)一步設(shè)計(jì)及改進(jìn)系統(tǒng)．SnpsGUI_v1．1主要集成了3個(gè)模塊:1)圖形用戶接口(GUI)模塊，是基于XBase++平臺(tái)開(kāi)發(fā)，為用戶提供簡(jiǎn)潔友好的實(shí)驗(yàn)和仿真界面;2)推理工具模塊，是基于SWI-Prolog技術(shù)開(kāi)發(fā)，該模塊完成系統(tǒng)模型的初始配置、連接和規(guī)則，并以文本方式生成相應(yīng)的轉(zhuǎn)移圖;3)圖形化設(shè)計(jì)工具模塊，它實(shí)現(xiàn)了提供給用戶友好的設(shè)計(jì)界面，如方便地添加、刪除神經(jīng)元節(jié)點(diǎn)、連接箭頭線以及各種規(guī)則．下面我們使用SnpsGUI_v1．1仿真軟件來(lái)實(shí)現(xiàn)一個(gè)產(chǎn)生數(shù)集的脈沖神經(jīng)膜系統(tǒng)形式化驗(yàn)證的仿真，從而獲得系統(tǒng)的格局轉(zhuǎn)移圖．一個(gè)如圖1所示的脈沖神經(jīng)膜系統(tǒng)∏，暫且假設(shè)我們不知道該系統(tǒng)具體功能，通過(guò)SnpsGUI_v1．1軟件的仿真獲得的系統(tǒng)格局轉(zhuǎn)移圖，看是否能確定其功能并驗(yàn)證其正確性和完整性?首先要給仿真器提供數(shù)據(jù)輸入．由于圖中有未知數(shù)r和n，而仿真必須有確定數(shù)目的神經(jīng)元，我們先假設(shè)r=2，n=4，則神經(jīng)元個(gè)數(shù)為9(包括環(huán)境ENV)，神經(jīng)元標(biāo)簽分別規(guī)定為1=1、2=2、3=3、4=4、d1=5、d2=6、out=7、0=8、ENV=9．圖2即是該脈沖神經(jīng)膜系統(tǒng)∏的輸入文件，輸入文件包括rule(規(guī)則)、synapses(連接關(guān)系)和initial(初始格局值)三項(xiàng)內(nèi)容，關(guān)于它們的釋義詳見(jiàn)文獻(xiàn)［7］．

通過(guò)執(zhí)行輸入文件，仿真軟件自動(dòng)生成9個(gè)PS文件和9個(gè)JPG圖片，分別對(duì)應(yīng)9步計(jì)算過(guò)程的格局轉(zhuǎn)移圖，圖3為第9步的轉(zhuǎn)移圖，說(shuō)明該系統(tǒng)在第9步后轉(zhuǎn)移圖再無(wú)新的格局產(chǎn)生．3．2轉(zhuǎn)移圖分析下面對(duì)這9步轉(zhuǎn)移圖進(jìn)行分析．由第1步轉(zhuǎn)移圖可知，標(biāo)簽為9的ENV神經(jīng)元(環(huán)境)接收到一個(gè)脈沖，由第7步轉(zhuǎn)移圖可知，ENV再次接收到一個(gè)脈沖，說(shuō)明該脈沖神經(jīng)膜系統(tǒng)∏是一個(gè)數(shù)的產(chǎn)生裝置，且數(shù)字6必是其數(shù)集中的元素(第7步與第1步的步數(shù)間隔為6);分析第6步轉(zhuǎn)移圖，發(fā)現(xiàn)產(chǎn)生一個(gè)二重分支，這是因?yàn)闃?biāo)簽為8的神經(jīng)元存在兩條不確定性的激發(fā)規(guī)則所致，跟蹤到第9步轉(zhuǎn)移圖，二重分支最終形成了兩個(gè)閉環(huán)，左邊閉環(huán)正是選擇了第2條激發(fā)規(guī)則(a→a;1)的路徑，右邊閉環(huán)則對(duì)應(yīng)了第1條激發(fā)規(guī)則(a→a;0)的路徑，而只有選擇右邊閉環(huán)才會(huì)有數(shù)產(chǎn)生(ENV接收到脈沖)，由于閉環(huán)存在，且圖中無(wú)停止格局，說(shuō)明該系統(tǒng)∏是一個(gè)不停止系統(tǒng)，即是產(chǎn)生無(wú)限數(shù)集的裝置;再仔細(xì)分析兩個(gè)閉環(huán)可知，左邊的閉環(huán)有4步，右邊的閉環(huán)有6步，意味著每多選擇一次左邊閉環(huán)路徑，產(chǎn)生的數(shù)的數(shù)值必然增加4，左邊閉環(huán)路徑的長(zhǎng)度為4i;i≥1，i表示產(chǎn)生某個(gè)數(shù)時(shí)連續(xù)選擇第2條激發(fā)規(guī)則(a→a;1)的次數(shù)．由于選擇右邊的閉環(huán)路徑會(huì)產(chǎn)生數(shù)的輸出，所以選擇右邊閉環(huán)的次數(shù)即是產(chǎn)生數(shù)的個(gè)數(shù)，而右邊閉環(huán)路徑長(zhǎng)度為6，因此可推導(dǎo)出該系統(tǒng)∏是一個(gè)產(chǎn)生{2+4i;i≥1}數(shù)集的裝置．兩個(gè)閉環(huán)在這里可理解為一個(gè)兩層嵌套循環(huán)，左邊閉環(huán)代表內(nèi)循環(huán)(循環(huán)變量為大于等于0的不確定值)，右邊閉環(huán)代表外循環(huán)(循環(huán)變量為無(wú)窮大);以上是在假設(shè)r=2，n=4的情況下推導(dǎo)出系統(tǒng)∏是一個(gè)產(chǎn)生{2+4i;i≥1}數(shù)集的裝置．