可移动类进程代数及其静态分析技术在系统生物学领域中应用的研究

论文摘要

可移动类进程代数是为描述可移动进程及通讯连接动态构成的进程网络而对传统抽象演算的扩展,为有效地计算系统的动态行为和运行的拓扑结构,本文开发了该类演算基于控制流分析和抽象解释的静态分析策略,并把系统生物学作为一个重要的应用领域。主要工作如下:开发了Mobile Ambients演算和Boxed Ambients演算的基于环境和能力出现次数的抽象解释技术。在演算的语法和语义规则中引进静态名字和捆绑器,分别标识约束名字和输入动作中引进的变量,使得静态分析结果在α-变换下恒等。开发了BioAmbients演算和Mobile Safe Ambients演算的控制流分析技术。在进程抽象表示的基础上,通过识别可被激活的移动能力探明环境的层次体系变化、通过识别可被激活的通讯能力确定变量与静态名字的捆绑关系,有效地计算系统运行的拓扑结构。应用可移动类进程代数描述具体的生物系统,分别建立了ABC转运器的π-演算模型及Na+-K+ATP酶的BioAmbients演算模型。应用基于控制流分析的静态分析技术对基于BioAmbients演算的Na+-K+ATP酶系统的动态行为和属性进行了分析和验证。研究结果显示:可移动类进程代数是一种很有前途的系统生物学的形式化工具,其静态分析技术是系统生物学的一种可靠的分析和验证工具。

论文目录

• 提要
• 第一章 绪论
• 1.1 进程代数
• 1.2 静态程序分析
• 1.3 系统生物学
• 1.4 系统生物学与可移动类进程代数
• 1.5 本文主要工作和本文组织结构
• 1.5.1 本文主要工作
• 1.5.2 本文组织结构
• 第二章 可移动类进程代数
• 2.1 引言
• 2.2 π-演算
• 2.3 Mobile Ambients演算
• 2.4 Mobile Safe Ambients演算
• 2.5 Boxed Ambients演算
• 2.6 BioAmbients演算
• 2.7 本章总结
• 第三章 可移动类进程代数的抽象解释
• 3.1 引言
• 3.2 抽象解释
• 3.3 基于环境和能力计数的Mobile Ambients演算的抽象解释
• 3.3.1 Mobile Ambients演算的扩展
• 3.3.2 抽象论域
• 3.3.3 抽象函数
• 3.3.4 抽象归约规则
• 3.3.5 抽象解释
• 3.3.6 抽象解释的正确性
• 3.4 Boxed Ambients演算的抽象解释
• 3.4.1 Boxed Ambients演算的扩展
• 3.4.2 抽象论域
• 3.4.3 抽象转换函数
• 3.4.4 抽象归约规则
• 3.4.5 基于抽象解释的Boxed Ambients演算的静态分析策略及其属性
• 3.5 本章小结
• 第四章 可移动类进程代数的控制流分析
• 4.1 引言
• 4.2 BioAmbients演算的控制流分析
• 4.2.1 BioAmbients演算的扩展
• 4.2.2 BioAmbients演算的抽象表示
• 4.2.3 BioAmbients演算的控制流分析的定义
• 4.2.4 BioAmbients演算的控制流分析的计算
• 4.2.5 BioAmbients演算的控制流分析的属性
• 4.3 Mobile Safe Ambients演算的控制流分析
• 4.3.1 Mobile Safe Ambients演算的扩展
• 4.3.2 Mobile Safe Ambients演算的抽象表示
• 4.3.3 Mobile Safe Ambients演算的控制流分析的定义
• 4.3.4 Mobile Safe Ambients演算控制流分析的初始化
• 4.3.5 Mobile Safe Ambients演算控制流分析的最小不动点计算
• 4.3.6 Mobile Safe Ambients演算的控制流分析的正确性
• 4.3.7 分析实例
• 4.4 本章小结
• 第五章 可移动类进程代数及其静态分析技术在系统生物学领域的应用
• 5.1 引言
• +-K⁺ATP酶的BioAmbients演算模型及其分析'>5.2 Na⁺-K⁺ATP酶的BioAmbients演算模型及其分析
• +-K⁺ATP酶'>5.2.1 Na⁺-K⁺ATP酶
• +-K⁺ATP酶的抽象表示'>5.2.2 基于BioaAmbients演算的Na⁺-K⁺ATP酶的抽象表示
• +-K⁺ATP酶的BioaAmbients演算模型的归约'>5.2.3 Na⁺-K⁺ATP酶的BioaAmbients演算模型的归约
• +-K⁺ATP酶的BioaAmbients演算模型的静态分析'>5.2.4 基于控制流的Na⁺-K⁺ATP酶的BioaAmbients演算模型的静态分析
• 5.3 基于π-演算的ABC转运器的表示
• 5.3.1 ABC转运器
• 5.3.2 ABC转运蛋白的π-演算模型
• 5.3.2.1 细胞外液的模型
• 5.3.2.2 底物捆绑蛋白模型
• 5.3.2.3 核苷酸结合域模型
• 5.3.2.4 ABC转运蛋白的构象模型
• 5.3.2.5 细胞内液模型
• 5.3.2.6 ABC转运系统的π—演算模型
• 5.3.3 ABC转运蛋白的π-演算模型的验证
• 5.4 本章小结
• 第六章 总结
• 6.1 完成的工作
• 6.2 不足之处及研究展望
• 参考文献
• 攻读博士学位期间已发表和已录用的学术论文
• 摘要
• Abstract
• 致谢