ABC转运器的π-演算模型及其验证  

A π-Calculus Model and Verification of ABC Transporter

作　　者：张红[1] 刘磊[1] 

机构地区：[1]吉林大学计算机科学与技术学院,长春130012

出　　处：《计算机研究与发展》2008年第z1期118-123,共6页Journal of Computer Research and Development

基　　金：吉林省科技发展计划基金项目(20050527)

摘　　要：将描述并行、分布式和可移动系统的进程代数应用于系统生物学的形式化描述和行为模拟,给出了SBP依赖式ABC转运器的π-演算模型,分析了其基于状态迁移规则的动态行为演变和构象变化过程,并用自动验证π-演算、通信系统演算CCS的移动工作台MWB对该模型进行了状态跟踪和性能验证.π-演算能够在统一的框架之下捕获分子生物系统的两个关键属性:模块化组织和动态行为,对其既能进行质的又能进行量的推理,证明了π-演算用于分子生物过程抽象描述的可行性.In order to apply calculi specifically designed to describe concurrent, distributed and mobile systems to the new domain of systems biology, a π-calculus model of SBP-dependent uptake ABC transporter is presented. Its evolvement of dynamic behavior as well as its transformation of architecture is particularly analyzed. Its essential properties and the states of the model are traced using MWB (mobility workbench used to verify processes in CCS or π-calculus automatically). These attempts highlight the promise in using π-calculus for the abstraction of systems biology. π-calculus can capture two essential properties of the molecular biological systems in one unifying framework: their molecular organizations and their dynamic behaviors, and allows both the qualitative and quantitative reasoning on these systems' properties.

关 键 词：进程代数 Π-演算 系统生物学 ABC转运器 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]