跳到主要内容

PRISM 生物系统建模

引言​

生物系统通常涉及复杂的随机行为和分子间相互作用，例如基因调控网络或细胞信号通路。PRISM作为一种概率符号模型检测器，能够对这类系统进行数学建模，并通过概率计算验证其性质。本章将介绍如何用PRISM构建生物系统模型，并通过案例演示关键分析步骤。

生物系统建模基础​

生物系统的PRISM建模通常基于以下要素：

  1. 离散状态空间：如分子浓度分级或基因表达状态。
  2. 概率转移：化学反应的概率性结果。
  3. 时间参数：连续时间马尔可夫链(CTMC)或离散时间模型。

示例：简单基因调控网络​

考虑一个基因的激活/抑制切换系统：

// 定义布尔变量表示基因状态
const bool ON;  // 初始状态由以下公式定义
formula init_state = !ON;

// 激活概率率（当OFF时）
const double activation_rate = 0.1;
// 抑制概率率（当ON时）
const double inhibition_rate = 0.05;

module Gene
  ON : bool init false;

  [activate] !ON -> activation_rate : (ON'=true);
  [inhibit] ON -> inhibition_rate : (ON'=false);
endmodule

案例研究：蛋白质相互作用网络​

系统描述​

建模两种蛋白质（A和B）的相互作用：

  1. 蛋白质A可自发形成二聚体（A+A→A₂）
  2. 蛋白质B能降解A₂
  3. 所有反应遵循质量作用动力学

PRISM 模型实现​

ctmc

// 反应速率常数
const double k1 = 0.02; // A+A → A₂
const double k2 = 0.1;  // A₂ → A+A
const double k3 = 0.01; // B + A₂ → B

// 分子计数上限
const int MAX = 100;

module ProteinA
  A : [0..MAX] init 50;  // 初始A分子数

  [dimerize] A >= 2 -> k1*A*(A-1)/2 : (A'=A-2);
  [dissociate] true -> k2 : (A'=A+2);
endmodule

module ProteinB
  B : [0..MAX] init 20;
  A2 : [0..MAX] init 0;

  [degrade] B >= 1 & A2 >=1 -> k3*B*A2 : (B'=B-1) & (A2'=A2-1);
endmodule

性质验证示例​

检查"A₂浓度在100小时内不超过10的概率"：

P=? [ F<=100 A2 > 10 ]

实际应用：细菌趋化性模型​

系统动力学​

PRISM 实现要点​

// 受体状态定义
formula inactive = (CheR_active < threshold);
[activate] inactive -> k_act * ligand_conc : (CheR_active'=min(CheR_active+1,MAX));
生物参数化建议
  1. 使用文献中的实验数据确定速率常数
  2. 分子计数范围应覆盖生理浓度
  3. 时间单位需与实际观测尺度一致

总结与扩展​

关键学习点​

  • 生物系统适合用CTMC模型描述
  • PRISM可通过分子计数或浓度分级表示生物状态
  • 概率时序逻辑能表达生物系统的动态性质

推荐练习​

  1. 扩展蛋白质模型加入抑制反馈机制
  2. 验证基因振荡器的周期性性质
  3. 比较离散计数与连续近似模型的差异

延伸资源​

  • PRISM官方生物案例库
  • 《系统生物学中的计算方法》第7章
  • SBML到PRISM的模型转换工具