Probabilistic model checking of the PDGF signaling pathway

In this paper, we apply the probabilistic symbolic model checker PRISM to the analysis of a biological system --- the Platelet-Derived Growth Factor (PDGF) signaling pathway, demonstrating in detail how this pathway can be analyzed in PRISM. Moreover, we compare the results from verification and ODE simulation on the PDGF pathway and demonstrate by examples the influence of model structure, parameter values and pathway length on the two analysis methods.