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

脈沖神經膜系統的定義及相關概念

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

脈沖神經膜系統形式化驗證仿真與分析

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

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