A checkpoints capturing timing-robust Boolean model of the budding yeast cell cycle regulatory network

To construct a timing-robust Boolean model that preserves checkpoint conditions of the budding yeast cell cycle, we used a model verification technique, ‘model checking’. By utilizing automatic and exhaustive verification of model checking, we found that previous models cannot properly capture essential checkpoint conditions in the presence of timing variations. In particular, such models violate the M phase checkpoint condition so that it allows a division of a budding yeast cell into two before the completion of its full DNA replication and synthesis. In this paper, we present a timing-robust model that preserves all the essential checkpoint conditions properly against timing variations. Our simulation results show that the proposed timing-robust model is more robust even against network perturbations and can better represent the nature of cell cycle than previous models.To our knowledge this is the first work that rigorously examined the timing robustness of the cell cycle process of budding yeast with respect to checkpoint conditions using Boolean models. The proposed timing-robust model is the complete state-of-the-art model that guarantees no violation in terms of checkpoints known to date.A cell must undergo the process of duplicating all its components and separating them, more or less evenly, to two daughter cells such that each daughter has the information and dynamics necessary to repeat the process. Such cell cycle dynamics are known in more detail for the budding yeast, Saccharomyces cerevisiae, compared to other eukaryotic organism [1,2]. The cell cycle process of budding yeast consists of four phases: G1, S, G2, and M. Initiated by stimulation of the G1 stationary phase, the cell cycle sequence proceeds (i.e., G1→S→G2→M) and finally returns to the G1 stationary phase. It is important to reach the final phase after completing each phase properly since any mistakes can cause significant defect to the cell cycle process. Hence, a cell verifies whether es