关于对PDGF信号路径进行概率模型检测的问题研究

发布时间：2018-06-07 04:09

本文选题：形式化方法 + 概率模型验证　；参考：《山东大学》2012年硕士论文

【摘要】：近年来,越来越多的计算机科学方法被广泛应用到诸如生物学等领域。一方面,计算机科学的方法可以通过在计算机上进行模拟等方式使得对问题的研究可以摆脱原本复杂的实验环境和条件,大大节约了研究成本和研究时间,降低了研究难度;另一方面,计算机领域方法的多样性和计算机的强大计算能力,为复杂问题的解决提供了可能性。由于系统生物学和计算机科学研究中的复杂分布式系统有着类似的地方,形式化方法领域中的模型和验证技术可以被应用到系统生物学领域。形式化方法在分析大型系统方面优势明显,它有着高效的验证技术,可以利用自动化的计算机工具分析具有复杂行为的大型系统。作为一种表现良好的形式化方法,概率模型验证方法近年来广受人们的关注与研究。概率模型验证是从定量方面去检查一个具有随机性行为的有限状态系统的正确性。它与已有的基于仿真的方法有着一个明显的区别是它能对所要验证的系统进行彻底地挖掘,而不是仅仅挖掘系统的一个子集。本文将概率模型验证的方法应用到分析PDGF生物信号路径系统中。首先,作为本文的理论基础,本文详细讨论了概率模型验证的相关概念及理论推演。概率模型验证需要用到两种输入,即对系统的详细描述以及对系统属性的详细描述。本文首先给出了概率模型验证的含义以及对系统详细描述的方法,讨论了所要验证系统的瞬时概率和稳定概率的计算方法。接下来本文讨论了系统属性的描述方法,详细给出了文中用到的语言——CSL(持续概率逻辑),并对其扩展,即回报属性进行了讨论。另外,本文给出了关于文中所用的概率模型验证工具PRISM的详细介绍。其次,本文所要分析的PDGF生物信号路径系统对于细胞的繁殖和生长具有重要意义,它直接调控细胞分裂和增殖,与癌症的产生密切相关。本文详细分析了其组成,并将对其的研究细化为三个具体的目标,从而实现对PDGF生物信号路径的更好理解。再次,本文通过三组实验来实现了对三个目标的分析。实验中本文采用通过添加／移除单一反应来进行比较分析的方法,创建了多个模型的变种,以此来研究某一反应对路径信号的影响。这三组实验的结果显示,定量验证的方法能够帮助我们更加深刻的理解PDGF信号路径,更进一步地,能够提供一个关于路径行为的预测。最后,由于除了概率模型验证方法,许多基于仿真的方法在研究生物系统时也非常流行,本文选择了其中的常微分方程方法将其与概率模型验证方法进行了比较研究。对常微分方法的研究分为理论与实践两部分。理论方面,本文首先给出了常微分方程在生物系统中的概念,然后为了更好地与概率模型验证方法进行比较,本文详细讨论了常微分方法中瞬时状态行为与稳定状态行为的计算。在实践方面,本文给出了用常微分方法分析PDGF信号路径的详细实验过程,并将实验结果与概率模型验证方法的结果进行了比较分析。两种方法所的结果较为类似,本文进一步分析了两种方法类似与不同的原因。
[Abstract]:In recent years, more and more computer science methods have been widely used in such fields as biology. On the one hand, the method of computer science can make the research of the problem free from the original complex experimental environment and conditions, and greatly save the research cost and the research time and reduce the research. On the other hand, the diversity of the computer domain method and the powerful computing power of the computer provide the possibility for the solution of complex problems. Because the complex distributed system in the system biology and computer science research has the similar place, the model and verification technology in the formal method domain can be applied to the system. In the field of biology, the formalization method has an obvious advantage in the analysis of large systems. It has an efficient verification technique and can use automated computer tools to analyze large systems with complex behavior.
As a formalized method with good performance, probability model verification method has been widely concerned and studied in recent years. The probability model verification is the validity of checking a finite state system with random behavior from the quantitative aspect. It has a distinct difference from the existing simulation based method that it can be tested. The system of certificates is thoroughly excavated, rather than just mining a subset of the system.
In this paper, the method of probabilistic model validation is applied to the analysis of PDGF biological signal path system.
First, as the theoretical basis of this paper, this paper discusses the related concepts and theoretical deduction of probability model verification in detail. The probability model verification needs two kinds of input, that is, detailed description of the system and detailed description of the system properties. In this paper, the method of describing the instantaneous probability and the stability probability of the system is discussed. In this paper, the description method of the system property is discussed, and the language used in the paper is given in detail, CSL (continuous probability logic), and its extension, that is, the return attribute is discussed. In addition, this paper gives the verification of the probability model used in the paper. A detailed introduction to the tool PRISM.
Secondly, the PDGF biosignal pathway system in this paper is of great significance to cell reproduction and growth. It directly regulates cell division and proliferation and is closely related to the production of cancer. This paper analyzes its composition in detail, and will refine its research into three specific targets, thus realizing the PDGF biological signal path. Good understanding.
Thirdly, in this paper, the analysis of three targets is realized through three groups of experiments. In the experiment, we use the method of adding / removing the single reaction to make a comparison and analysis, and create a variety of models, in order to study the effect of a reaction on the path signal. The results of the three groups of tests show that the method of quantitative verification can help. To help us understand the PDGF signal path more deeply, we can further provide a prediction of path behavior.
Finally, in addition to the probability model verification method, many simulation based methods are also very popular in the study of biological systems. This paper chooses the ordinary differential equation method to compare it with the probability model verification method. The study of the ordinary differential method is divided into two parts: Theory and practice. The concept of the ordinary differential equation in the biological system is given, and in order to compare with the probability model verification method better, the calculation of the instantaneous state behavior and the stable state behavior in the ordinary differential method is discussed in detail. In practice, the detailed experimental process of the analysis of the PDGF signal path by the ordinary differential method is given in this paper. The experimental results are compared with the results of the probabilistic model verification method. The results of the two methods are similar. This paper further analyzes the reasons for the similarity and difference between the two methods.
【学位授予单位】：山东大学
【学位级别】：硕士
【学位授予年份】：2012
【分类号】：Q811

【共引文献】