Wei Ou, Guo Zonghao, Niu Yun, Liao Wenyuan
Department of Computer Science, Nanjing University of Aeronautics and Astronautics, Nanjing, China.
Department of Mathematics and Statistics, University of Calgary, Calgary, Canada.
BMC Syst Biol. 2017 Dec 14;11(Suppl 6):104. doi: 10.1186/s12918-017-0481-6.
Probabilistic Boolean networks (PBNs) have been proposed for analyzing external control in gene regulatory networks with incorporation of uncertainty. A context-sensitive PBN with perturbation (CS-PBNp), extending a PBN with context-sensitivity to reflect the inherent biological stability and random perturbations to express the impact of external stimuli, is considered to be more suitable for modeling small biological systems intervened by conditions from the outside. In this paper, we apply probabilistic model checking, a formal verification technique, to optimal control for a CS-PBNp that minimizes the expected cost over a finite control horizon.
We first describe a procedure of modeling a CS-PBNp using the language provided by a widely used probabilistic model checker PRISM. We then analyze the reward-based temporal properties and the computation in probabilistic model checking; based on the analysis, we provide a method to formulate the optimal control problem as minimum reachability reward properties. Furthermore, we incorporate control and state cost information into the PRISM code of a CS-PBNp such that automated model checking a minimum reachability reward property on the code gives the solution to the optimal control problem. We conduct experiments on two examples, an apoptosis network and a WNT5A network. Preliminary experiment results show the feasibility and effectiveness of our approach.
The approach based on probabilistic model checking for optimal control avoids explicit computation of large-size state transition relations associated with PBNs. It enables a natural depiction of the dynamics of gene regulatory networks, and provides a canonical form to formulate optimal control problems using temporal properties that can be automated solved by leveraging the analysis power of underlying model checking engines. This work will be helpful for further utilization of the advances in formal verification techniques in system biology.
概率布尔网络（PBNs）已被提出用于分析基因调控网络中的外部控制，并纳入了不确定性。具有扰动的上下文敏感PBN（CS-PBNp）扩展了具有上下文敏感性的PBN以反映内在的生物稳定性，并通过随机扰动来表达外部刺激的影响，被认为更适合于对受外部条件干预的小型生物系统进行建模。在本文中，我们应用概率模型检验这一形式化验证技术，对CS-PBNp进行最优控制，以在有限控制时域内最小化预期成本。
我们首先描述了使用广泛使用的概率模型检验器PRISM提供的语言对CS-PBNp进行建模的过程。然后我们分析了基于奖励的时态属性以及概率模型检验中的计算；基于该分析，我们提供了一种将最优控制问题表述为最小可达性奖励属性的方法。此外，我们将控制和状态成本信息纳入CS-PBNp的PRISM代码中，使得对该代码自动进行最小可达性奖励属性的模型检验能够给出最优控制问题的解。我们在两个示例上进行了实验，一个是细胞凋亡网络，另一个是WNT5A网络。初步实验结果表明了我们方法的可行性和有效性。
基于概率模型检验的最优控制方法避免了与PBN相关的大规模状态转移关系的显式计算。它能够自然地描述基因调控网络的动态特性，并提供一种规范形式，利用时间属性来表述最优控制问题，这些问题可以通过利用底层模型检验引擎的分析能力自动求解。这项工作将有助于进一步利用形式化验证技术在系统生物学方面的进展。
