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

Executable Specification of P Systems with Active Membranes and Its Implementation

作　　者：张民[1] 戚正伟[2] 董笑菊[1] 

机构地区：[1]上海交通大学电子信息与电气工程学院,上海200240 [2]上海交通大学软件学院,上海200240

出　　处：《上海交通大学学报》2008年第10期1635-1639,共5页Journal of Shanghai Jiaotong University

基　　金：国家重点基础研究发展规划(973)项目(2003CB317005);国家自然科学基金资助项目(60573002;60703033);高等学校博士学科点基金资助项目(20010248033)

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

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

分 类 号：TP301.2[自动化与计算机技术—计算机系统结构]