摘要：膜计算是自然计算的新分支,是计算机科学、数学、生物学等众多学科交叉的研究领域,旨在从细胞的结构和功能,以及从组织和器官等细胞群相互协作处理信息的方式中,抽象出新的计算模型,也称为膜系统或P系统。脉冲神经膜系统是膜计算中的一种神经型P系统,是源于大脑神经元之间通过电脉冲进行信息传递的生物现象,并吸收脉冲神经网络的特点而提出的一种新型的分布式、并行计算模型。本文从计算理论、应用和软件仿真研究三个方面分别对几类脉冲神经膜系统的计算能力、小通用性、逻辑与算术运算实现方法以及模型的形式化验证等内容进行了研究,主要工作如下：研究了同质脉冲神经膜系统的小通用性：在使用标准规则和权值情况下,作为计算函数的装置,需要53个神经元可以构造一个通用同质脉冲神经膜系统；作为产生数的装置,则需要52个神经元。研究脉冲神经膜系统的小通用性问题既具有计算机科学上的意义,也具有生物学上的用义：寻找小通用“脑”。研究了突触上带权值和突触上不带权值的两种同质脉冲神经膜系统在不使用具有延迟的激发规则情况下的计算通用性问题,并证明了这两种不带延迟的同质脉冲神经膜系统无论是工作在产生模式下,还是工作在接收模式下都是计算通用的。解决了曾湘祥等人提出的关于不带延迟的同质脉冲神经膜系统是否具有计算通用性的公开问题。同时,也构造了不使用延迟激发规则的突触上带权值和不带权值的两类同质延展脉冲神经膜系统,并证明了它们的计算通用性。研究了无延迟规则和突触权值情况下的带反脉冲同质脉冲神经膜系统的计算通用性问题,证明了这种膜系统无论是工作在产生模式,还是接收模式下都是计算通用的。研究结果能同时解决了曾湘祥等人提出的关于是否存在无延迟规则的同质脉冲神经膜系统和如何有效移除突触权值的两个公开问题。考虑在脉冲神经膜系统这种装置上处理一些简单的逻辑与算术运算问题,构建了包括实现二进制补码转换、实现有符号整数的加、减法运算和实现任意两个自然数的乘法运算的多族脉冲神经膜系统,这些系统的输入、输出数均采用二进制方式,编码采用合适的脉冲序列。较好地解决了Gutierrez-Naranjo MA.和Leporati A.提出的关于如何实现两个任意自然数乘法运算的公开问题。当前工作可以作为解决更加复杂问题的基础,也有助于设计基于脉冲神经膜系统的生物型“CPU”。使用带反脉冲的脉冲神经膜系统分别构建了能实现对称三值的通用与、或、非逻辑门功能和实现对称三值的整数加、减算术运算功能的多族脉冲神经膜系统。目前的工作是基于带反脉冲的脉冲神经膜系统的三值型“CPU”设计在理论上的首次尝试,也为潘林强和Paun G提出的一个公开问题提供了首个实用案例。基于SnpsGUI仿真软件,例证了两个脉冲神经膜系统的形式化验证过程,重点分析并揭示了格局转移图和脉冲神经膜系统之间的内在联系,并总结出了三个一般性结论,达到了通过计算机辅助验证脉冲神经膜系统正确性与完整性的目的。同时,对基于脉冲神经膜系统更有效的形式化验证方法提出了展望,对SnpsGUI软件进行了评述,提出了改进方向。