华东师范大学学报(自然科学版) ›› 2018, Vol. 2018 ›› Issue (1): 59-75,90.doi: 10.3969/j.issn.1000-5641.2018.01.007

• 计算机科学 • 上一篇    下一篇

布尔网络到离散时间马尔科夫模型的转换及性质研究——以大鼠干细胞基因调控网络为例

吕悦1, 张敏2, 秦旭东1, 严佳1   

  1. 1. 华东师范大学 上海市高可信计算重点实验室, 上海 200062;
    2. 华东师范大学 计算机科学与软件工程学院, 上海 200062
  • 收稿日期:2016-12-09 出版日期:2018-01-25 发布日期:2018-01-11
  • 通讯作者: 张敏,女,副教授,研究方向为形式化验证.E-mail:mzhang@sei.ecnu.edu.cn. E-mail:mzhang@sei.ecnu.edu.cn
  • 作者简介:吕悦,女,硕士研究生,研究方向为形式化验证.E-mail:lvyue2013@foxmail.com.
  • 基金资助:
    国家自然科学基金(6167202)

The transition and properties from Boolean networks to discrete-time Markov chains: A case study of mice stem cell gene regulatory networks

LYU Yue1, ZHANG Min2, QIN Xu-dong1, YAN Jia1   

  1. 1. Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai 200062, China;
    2. School of Computer Science and Software Engineering, East China Normal University, Shanghai 200062, China
  • Received:2016-12-09 Online:2018-01-25 Published:2018-01-11

摘要: 提出了一种基于概率模型检测技术的新方法用于解决生物工程中基因调控网络探查吸引子这一关键问题.以大鼠干细胞基因调控网络的吸引子找寻这样一个具体问题为例,将布尔网络表示的基因调控网络的更新函数通过对应的真值表,转换为离散时间马尔科夫链,写入模型检测工具PRISM中;之后通过验证模型的系统性质的技术去验证每个基因在很长一段时间之后的激活概率,以此找到基因调控网络中的吸引子.同时,通过添加基因扰动的方式,改变每个基因的激活/抑制概率,可以找到每个基因对其他基因的促进/抑制关系.实验表明,大鼠干细胞基因中有7个基因在一段时间后状态不变,剩余基因的变化共同构成了一个吸引环.整个检测流程简洁易用,可以直接找出吸引子.进一步地,实验准确地找出了大鼠干细胞中Gata1基因的抑制/促进对象,此实验结果对解决大鼠的白血球减少症有着治疗方面的意义.

关键词: 布尔网络, 离散时间马尔科夫链, 基因调控网络

Abstract: This paper proposes a new method based on probabilistic model checking technique to solve the problem of detecting attractors in gene regulatory networks which is vital in bio-engineering. We transform a gene regulatory network into a discrete-time Markov chains (DTMC for short) by using truth table. We verify the possibility of gene activation in some "long term" through a model checker named PRISM, which help us to find attractors of the gene regulatory network. In this paper, we show the whole procedure using the example of mice stem cell gene regulatory networks. Meanwhile, we make a new technique of detecting the promotion/inhibition relations between genes by adding gene disturbance and modifying gene activation/suppression probability. We show that in the mice regulatory network, seven genes will remain their invariable states in some "long term", then the rest of "changing" genes forms a cyclic attractor. The experiment shows that our method can find the attractors easily and directly. Moreover, our experiment successfully finds those genes affected by gene Gata1, which would be helpful for studying the mice leucopenia.

Key words: Boolean networks, discrete-time Markov chains, gene regulatory network

中图分类号: