2021-4-9 | 网络工程论文
本文主要内容正是基于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}数集的装置．