使用模型检测解决概率布尔网络优化控制

系统生物学期望对复杂生物系统建立一个真实的、可计算的模型,以便于以系统的角度去理解生物系统的演变过程。在系统生物学中,一个重要的主题是通过外部的干预控制发展关于基因调控网络的控制理论,以作为未来基因治疗技术。目前,布尔网络及其扩展的概率布尔网络已经被广泛用于对基因调控网络进行建模。在控制问题的研究中,概率布尔控制网络的状态迁移本质上构成一条有限状态空间的离散时间马尔科夫决策过程。依据马尔科夫决策过程的理论,通过概率模型检测方法解决网络中有限范围优化控制问题和无限范围优化控制问题。针对带有随机干扰且上下文相关的概率布尔控制网络,使用概率模型检测器PRISM对其进行形式化建模,然后将两类优化控制问题描述为相应的时序逻辑公式,最后通过模型检测寻找出最优解。实验结果表明,提出的方法可以有效地用于生物网络的分析和优化控制。

Optimal Control of Probabilistic Boolean Networks Using Model Checking

Systems biology expected to construct a realistic and computational model of complex biology systems that aims at system-level understanding of biological systems.One of the significant topics in the field of system biology is that the control theory of gene regulatory networks (GRNs) is developed by applying external intervention control for gene theory technologies in the future.At present,Boolean networks and extended probabilistic Boolean networks have been used as the model of GRNs widely.In the research of control problem,the state transition of probabilistic Boolean control networks essentially forms a finite-state and discrete-time Markov decision processes (MDP).According to MDP theory,finite-horizon optimal control problem and infinite-horizon optimal control problem can be solved by using probabilistic model checking.For content-sensitive probabilistic Boolean control networks with random perturbation,probabilistic model checker PRISM is used to model formally.Then two kinds of optimal control problems are expressed by temporal logic.Finally,the optimal solution is found via model checking.The results indicate that this proposed approach can be used for analysis and optimal control of biology networks effectively.