论文摘要
随着计算机科学与其他学科之间的相互渗透和影响,科学家们根据不同原理提出了不同的计算模型。细胞膜计算是一种基于生物细胞膜结构和功能的新型计算模型,近年来得到广泛的研究。SN P系统（Spiking Neural P Systems）是对类神经细胞膜计算（Neural-like P Systems）的扩展。与其他细胞膜计算的不同的是,它在计算中引入了时间的概念,计算由一个全局时钟驱动。SN P系统已被证明具有与图灵机相同的计算能力。然而随着研究的深入,模型的设计越来越复杂,如何有效地验证模型的正确性和研究SN P系统的性质成为该领域当前一个迫切需要解决的问题。模型检测作为一种研究和验证系统性质的方法,可以有效地帮助我们解决这一问题。目前用于模型检测的工具主要有SPIN、Maude等。Maude是一种基于重写逻辑的形式化描述语言,由Maude解释器解释执行,主要用于模型检测和逻辑推理。[0]本文的主要工作是:通过扩展Maude中的重写规则语义,利用代数方法定义了SN P系统中计算规则的操作语义,并借助于Maude中面向对象的形式化描述,给出了SN P系统通用的描述方法,把SN P系统转化成为可执行的形式化描述。这种形式化的描述可以被Maude解释器解释运行,从而自动推导系统的计算结果、验证系统的某些性质等。最后,本文将这一形式化描述方法应用于具体的SN P系统模型并给出了验证的结果,证明了模型检测的可行性与正确性。本文的主要贡献是:将模型检测应用于SN P系统;利用Maude语言定义了SN P系统中计算规则的操作语义;给出了SN P系统在Maude下通用的形式化描述方法;达到了通过计算机辅助验证SN P系统正确性与完整性[0]的目的。
论文目录
摘要ABSTRACT第一章 绪论1.1 研究背景1.2 研究现状与问题1.3 本文的内容和结构第二章 SN P 系统及计算原理2.1 SN P 系统的生物学原理2.2 SN P 系统的定义2.3 SN P 系统的计算原理2.4 SN P 系统模型的应用实例2.5 本章小结第三章 重写逻辑理论与形式化描述3.1 关系等式理论3.2 重写逻辑理论3.3 MAUDE3.3.1 函数模块3.3.2 系统模块3.3.3 Maude 的面向对象性3.3.4 实时Maude3.4 本章小结第四章 SN P 系统在实时MAUDE 下的形式化描述4.1 SN P 系统结构的描述4.1.1 触发因子的定义4.1.2 神经元状态的定义4.1.3 神经元的定义4.1.4 神经元之间的通信4.2 SN P 系统规则的描述4.2.1 正则表达式的描述4.2.2 触发规则的描述4.2.3 遗忘规则的描述1 的形式化描述'>4.3 SN P 系统模型Π1的形式化描述4.4 本章小结第五章 SN P 系统模型检测的应用5.1 利用SN P 系统解决SAT 问题5.1.1 SAT 问题5.1.2 构造SN P 系统模型5.1.2.1 SN P 系统框架结构SAT 求解过程'>5.1.2.2 ΠSAT求解过程5.1.2.3 一个解决SAT 问题的SNP 系统实例SAT 模型的形式化描述与运行结果'>5.2 对ΠSAT模型的形式化描述与运行结果SAT 模型的形式化描述'>5.2.1 ΠSAT模型的形式化描述5.2.2 在Maude 下的运行结果5.3 本章小结第六章 工作总结与分析6.1 工作总结6.2 未来工作与展望参考文献附录1 的形式化描述'>附录I：MAUDE 对SN P 系统Π1的形式化描述SAT 的形式化描述'>附录II：MAUDE 对SN P 系统ΠSAT的形式化描述符号与标记致谢攻读硕士学位期间已发表或录用的论文
相关论文文献
标签：细胞膜计算论文; 系统论文; 重写逻辑论文; 模型检测论文;
