This model is an extension of the seminal model of the G1/S restriction point control of mammalian cell cycle, published by Fauré et al (2006) [1]. We have used model-checking and computing tree logics (CTL) to progressively refine Fauré's model in order to fit recent experimental observations. The resulting model accounts for the sequential activation of cyclins, the role of Skp2, and emphasizes a multifunctional role for the cell cycle inhibitor Rb.
We provide the models in different formats:
1) An archive containing the multilevel model, to be open with GINsim (v2.9.3).
2) An archive containing a Boolean translation of this model, to be open with GINsim (v2.9.3).
3) A SBML Qual export of the multilevel model.
4) A SBML Qual export of the Boolean version.
Furthermore, we provide a script containing the main NuSMV queries used in the article describing the methodology and the resulting revised model.
Multilevel mammalian cell cycle model
Summary: