本文主要内容正是基于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}数集的装置．#p#分页标题#e#
同理，我们可以再假设r=3，n=5的情况下进行形式化验证仿真从而获得系统的转移图，共计11步，通过同样的分析得出，在r=3，n=5的情况下，系统∏是一个产生{3+5i;i≥1}数集的装置．因此我们不难分析得出图1所示的脉冲神经膜系统∏的格局转移示意图(图4)及其功能是一个产生{r+ni;i≥1}数集装置的结论．下面对图4进行归纳性的分析、总结．首先规定:图4中C0表示来自采用神经元0中a→a;0规则的格局，C1表示来自采用神经元0中a→a;1规则的格局;δ表示c2→…→cr+2路径，τ表示cr+2→…→cr+n－1→c0r+n→c0r+n+1路径，则长度L(σ)=r，长度L(τ)=n－1．对于i≥o，规定γ(i)表示路径cr+2(i?→)…cr+n－1→c1r+n→c1r+n+1→c1r+2，意味着cr+2被通过了(i+1)次;δ(i)表示路径c2?→δcr+2γ(i?→)cr+2，则长度L(γ(i))=ni，L(δ(i))=r+ni．因此，对于系统∏的每次计算C存在一个不确定的整数i{ik:k≥1}，C在转移图上的路径为:c0→c1→c2δ(i1???→)cr+2?→τc0r+n+1→c2δ(i2???→)cr+2?→γc0r+n+1→．计算以C({ik:k≥1})表示，则:Nall(C(ik:k≥1}))={tk+1－tk:k≥1}={r+n(ik+1):k≥1}．最后结论:1)对于每一个n≥2，系统∏的每个计算C，N(C)?{r+ni;i≥1}；2)对于每个i≥1，都存在一个系统∏的计算C，满足r+ni∈N(C);3)结论1)验证了系统∏的正确性，结论2)验证了系统∏的完整性，最终验证了系统∏是一个产生数集{r+ni;i≥1}的装置．以上实例是基于数的产生装置的形式化验证，文献［9］研究了脉冲神经膜系统在使用广义规则时的语言产生能力，并通过系统∏1例证了转移图能有效地对脉冲神经膜语言产生装置进行形式化验证．基于SnpsGUI_v1．1，我们能自动生成文献［9］中系统∏1的转移图如图5，采用本文以上分析法，同样可验证系统∏1的正确性和完整性，系统∏1实际上可看成一个非确定性有限自动机(因为图中有停止格局存在)，它的功能是产生如下语言:L(∏1)=L((0*0(11∪111)*110)*0*(011∪0(11∪111)+(0∪02)1))．由以上分析可归纳出以下一般性结论:①具有有限格局的转移图能直观地反映出各类脉冲神经膜系统(数或语言产生装置)的计算过程;②选择规则的不确定性在转移图中是以多重选择来分支，分支数视神经元中不确定性规则数决定，假设只有一个神经元具有N条不确定性规则，则分支数必等于N;若有多个神经元具有多条不确定性规则，且某神经元具有最少的N条不确定性规则，则多重分支的分支数必大于或等于N;③不停止计算系统是以闭环(或循环)的方式且不存在停止格局在有限格局的转移图中得以体现，可停止计算系统是以存在停止格局在格局转移图中得以体现．通过以上分析，我们例证了格局转移图对于脉冲神经膜系统的形式化验证是有效的方法之一，而SnpsGUI_v1．1仿真软件能为我们自动生成需要的系统格局转移图．
总结及评述
本文基于SnpsGUI_v1．1仿真软件实现了脉冲神经膜系统形式化验证的仿真，并通过分析格局转移图，例证了假定系统的正确性和完整性，得出了格局转移图与脉冲神经膜系统之间的内在联系，并总结出了3个一般性结论．因此，格局转移图对于脉冲神经膜系统的形式化验证是有效的方法之一，而SnpsGUI_v1．1仿真软件能辅助我们自动地获得格局转移图，是一款基于脉冲神经膜系统形势化验证的教学和研究的有力辅助工具．格局转移图作为脉冲神经膜系统形式化验证的方法也存在其局限性．例如，对于比较复杂的脉冲神经膜系统，由于格局繁多，仅依靠格局转移图很难对计算过程进行有效的观测和分析，因此有必要寻找更有效的形式化的描述和验证手段．O．Andrei等人利用Maude的元语言(meta-language)特性定义了细胞型膜系统中规则的操作语义，给出了模型框架的一般表示方法［10］，这一方法可以移植到脉冲神经膜系统中使用，从而更有效地解决脉冲神经膜系统的形式化验证问题．基于脉冲神经膜系统的仿真软件SnpsGUI_v1．1虽然具有独创性、模块化、灵活性、界面友好等特点，但也存在一些需要改善的方面:1)扩展性不足．目前由于脉冲神经膜系统是一个研究热点，各种基于脉冲神经膜系统的变体不断涌现，如星型细胞控制型脉冲神经膜系统［11］等，该软件无法适应这类变体;其次，该软件只适合有限的7类规则，对于其它的规则，如穷举使用规则［12］等就无法适应．2)图形化设计模块存在一些小BUG，如图形化显示大小无法调整等．3)功能上有待提高，如可增加由数据输入文件自动生成系统模型图等辅助功能．
本文作者：彭献武 樊晓平 刘建勋 单位：中南大学信息科学与工程学院 湖南科技大学知识处理与网络化制造实验室 湖南财政经济学院网络化系统研究所