Research On Probabilistic Model Checking Of The PDGF Signaling Pathway

Recently, more and more techniques in the field of computer science have been applied to other fields like biology. For one thing, techniques of computer science can get rid of complex experiment environment and conditions with the help of simulation in a computer, and hence save research cost and time and reduce research difficulty; for another, methods of computer science are various and the computing capabilities are more and more powerful, making it possible to solve complex problems. Due to the similarity between biological systems and complex distributed systems studied in the field of computer science, modeling and analyzing techniques developed in the field of formal method can be applied to biological systems. Formal method has many advantages for analyzing large systems:it has effective verification techniques and can use computer tools to analyze large systems with complex behaviors automatically.As one well-performance formal method, probability model checking method has gain much attention and research recently. With focus on quantitative aspect, probability model checking aims at verifying a finite state system with stochastic behavior. Comparing to other simulation based method, one important advantage of probabilistic model checking is that it can explore the system exhaustively, not only explore a subset of the system.In this thesis, we apply probabilistic model checking to the analysis of a biological system-the Platelet-Derived Growth Factor (PDGF) signaling pathway.First of all, we discuss the concept of probabilistic model checking and related theory in details. Probabilistic model checking required two inputs:a description of the system and a specification of the system properties. In this thesis, we first give out the concept of probabilistic model checking and the method of describing a system. We discuss in details how the transient state probability and stead state probability are calculated. Then we give out how to specify the system properties using CSL (continuous stochastic logic), and discuss the extension of CSL, that is the reward property. Besides, we introduce the probabilistic model checking tool PRISM.Secondly, the PDGF signaling pathway system is of great importance to cellular production and growth; it regulates cellular division and proliferation directly and is highly related to the occurrence of cancer. In this thesis, we introduce the constitution of the PDGF signaling pathway and propose three goals to analyze the system in order to get a better understanding of the system.Moreover, we carry out three experiments to fulfill our three goals. In order to get the influence of a certain reaction to the signaling pathway, we build several models and do comparison work by adding/removing a certain reaction. The experiments results show that quantitative verification can give us a better understanding of the PDGF signaling pathway and more deeply it can give rise to a better behavior prediction of the pathway.Lastly, due to the fact that except for probabilistic model checking, many other simulation based method are also popular in analyzing biological systems, we choose ODE (ordinary differential equation) method and do comparing analyze between ODE and probabilistic model checking. The analysis of ODE can be divided into theoretical and practical parts. In the part of theory, we introduce the concept of ODE in the field of system biology. In order to get a better comparison between ODE and probabilistic model checking, we discuss in details how the transient state probability and steady state probability of the ODE method are calculated. In the part of practice, we apply the ODE method in analyzing the PDGF signaling pathway and do comparison between the results of ODE method and probabilistic model checking. The results of the two methods are similar. More deeply, we analyze the reason for the similarity of the two methods.