Hong Changki, Lee Minho, Kim Dongsup, Kim Dongsan, Cho Kwang-Hyun, Shin Insik
Department of Computer Science, KAIST, Daejeon, Korea.
BMC Syst Biol. 2012 Sep 28;6:129. doi: 10.1186/1752-0509-6-129.
Cell cycle process of budding yeast (Saccharomyces cerevisiae) consists of four phases: G1, S, G2 and M. Initiated by stimulation of the G1 phase, cell cycle returns to the G1 stationary phase through a sequence of the S, G2 and M phases. During the cell cycle, a cell verifies whether necessary conditions are satisfied at the end of each phase (i.e., checkpoint) since damages of any phase can cause severe cell cycle defect. The cell cycle can proceed to the next phase properly only if checkpoint conditions are met. Over the last decade, there have been several studies to construct Boolean models that capture checkpoint conditions. However, they mostly focused on robustness to network perturbations, and the timing robustness has not been much addressed. Only recently, some studies suggested extension of such models towards timing-robust models, but they have not considered checkpoint conditions.
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.
芽殖酵母(酿酒酵母)的细胞周期过程包括四个阶段:G1期、S期、G2期和M期。细胞周期由G1期的刺激引发,通过S期、G2期和M期的一系列过程回到G1静止期。在细胞周期中,细胞在每个阶段结束时验证是否满足必要条件(即检查点),因为任何阶段的损伤都可能导致严重的细胞周期缺陷。只有当检查点条件得到满足时,细胞周期才能正常进入下一阶段。在过去十年中,已有多项研究构建了捕捉检查点条件的布尔模型。然而,这些研究大多集中在对网络扰动的鲁棒性上,而时间鲁棒性并未得到太多关注。直到最近,一些研究才建议将此类模型扩展为时间鲁棒模型,但他们没有考虑检查点条件。
为了构建一个保留芽殖酵母细胞周期检查点条件的时间鲁棒布尔模型,我们使用了一种模型验证技术——“模型检查”。通过利用模型检查的自动和详尽验证,我们发现先前的模型在存在时间变化时无法正确捕捉基本的检查点条件。特别是,此类模型违反了M期检查点条件,从而允许芽殖酵母细胞在其完整的DNA复制和合成完成之前就分裂为两个细胞。在本文中,我们提出了一个时间鲁棒模型,该模型能够在时间变化的情况下正确保留所有基本的检查点条件。我们的模拟结果表明,所提出的时间鲁棒模型即使在面对网络扰动时也更具鲁棒性,并且比先前的模型能更好地反映细胞周期的本质。
据我们所知,这是第一项使用布尔模型严格研究芽殖酵母细胞周期过程在检查点条件方面的时间鲁棒性的工作。所提出的时间鲁棒模型是目前最先进的完整模型,保证了在已知检查点方面不会出现违反情况。