上海交通大学学报

上海交通大学学报（自然版）

• 自动化技术、计算机技术 • 上一篇    下一篇

活性细胞膜计算的可执行性描述与实现

张民a，戚正伟b，董笑菊a   

  1. (上海交通大学 a.电子信息与电气工程学院; b.软件学院, 上海 200240)
  • 收稿日期:2007-11-11 修回日期:1900-01-01 出版日期:2008-10-28 发布日期:2008-10-28
  • 通讯作者: 董笑菊

Executable Specification of P Systems with Active Membranes and Its Implementation

ZHANG Minaa,QI Zheng-weib,DONG Xiao-jua   

  1. (a.School of Electronic, Information and Electrical Engineering; b.School of Software,
    Shanghai Jiaotong University, Shanghai 200240, China)
  • Received:2007-11-11 Revised:1900-01-01 Online:2008-10-28 Published:2008-10-28
  • Contact: DONG Xiao-ju

摘要： 基于重写逻辑理论，利用Maude语言对活性细胞膜计算模型进行可执行性描述，实现了借助于计算机自动验证计算模型的正确性、完整性，以及辅助研究模型的性质等功能.通过采用Maude语言对活性细胞膜计算中6条基本规则的定义，给出了模型通用的描述方法.利用该方法描述与验证了可满足性问题在活性细胞膜计算中的模型.通过对计算结果的分析，说明了方法的可行性与正确性.

关键词: 活性细胞膜计算, 重写逻辑, 可满足性问题

Abstract: Based on rewriting logic, an executable specification method was proposed to specify the P systems with active membranes (PSAM) in Maude language. The purpose is to check the correctness of the model automatically and study the properties of PSAM with the help of computer. Six formal specifications were defined in Maude respectively for the six basic rules in PSAM, so that any given PSAM model can be specified formally. An example was presented to demonstrate how to specify the PSAM model, which is used to solve SAT Problem. The feasibility and correctness of the specification method are concluded practically, with the analysis of the result that is reduced by running the specification in Maude.

中图分类号: