Formal verification confirms the role of p53 protein in cell fate decision mechanism.

The bio-cell cycle is controlled by a complex biochemical network of signaling pathways. Modeling such challenging networks accurately is imperative for the understanding of their detailed dynamical behavior. In this paper, we construct, analyze, and verify a hybrid Petri net (HPN) model of a complex biochemical network that captures the role of an important protein (namely p53) in deciding the fate of the cell. We model the behavior of the cell nucleus and cytoplasm as two stochastic and continuous Petri nets, respectively, combined together into a single HPN. We use simulative model checking to verify three different properties that capture the dynamical behavior of p53 protein with respect to the intensity of the ionizing radiation (IR) to which the cell is exposed. For each IR dose, 1000 simulation runs are carried out to verify each property. Our verification results showed that the fluctuations in p53, which relies on IR intensity, are compatible with the findings of the preceding simulation studies that have previously examined the role of p53 in cell fate decision.