{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,31]],"date-time":"2026-01-31T07:14:48Z","timestamp":1769843688491,"version":"3.49.0"},"reference-count":56,"publisher":"Oxford University Press (OUP)","issue":"17","license":[{"start":{"date-parts":[[2016,11,10]],"date-time":"2016-11-10T00:00:00Z","timestamp":1478736000000},"content-version":"vor","delay-in-days":73,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016,9,1]]},"abstract":"<jats:title>Abstract<\/jats:title>\n               <jats:sec>\n                  <jats:title>Motivation<\/jats:title>\n                  <jats:p>Understanding the temporal behaviour of biological regulatory networks requires the integration of molecular information into a formal model. However, the analysis of model dynamics faces a combinatorial explosion as the number of regulatory components and interactions increases.<\/jats:p>\n               <\/jats:sec>\n               <jats:sec>\n                  <jats:title>Results<\/jats:title>\n                  <jats:p>We use model-checking techniques to verify sophisticated dynamical properties resulting from the model regulatory structure in the absence of kinetic assumption. We demonstrate the power of this approach by analysing a logical model of the molecular network controlling mammalian cell cycle. This approach enables a systematic analysis of model properties, the delineation of model limitations, and the assessment of various refinements and extensions based on recent experimental observations. The resulting logical model accounts for the main irreversible transitions between cell cycle phases, the sequential activation of cyclins, and the inhibitory role of Skp2, and further emphasizes the multifunctional role for the cell cycle inhibitor Rb.<\/jats:p>\n               <\/jats:sec>\n               <jats:sec>\n                  <jats:title>Availability and Implementation<\/jats:title>\n                  <jats:p>The original and revised mammalian cell cycle models are available in the model repository associated with the public modelling software GINsim (http:\/\/ginsim.org\/node\/189).<\/jats:p>\n               <\/jats:sec>\n               <jats:sec>\n                  <jats:title>Contact<\/jats:title>\n                  <jats:p>thieffry@ens.fr<\/jats:p>\n               <\/jats:sec>\n               <jats:sec>\n                  <jats:title>Supplementary information<\/jats:title>\n                  <jats:p>Supplementary data are available at Bioinformatics online.<\/jats:p>\n               <\/jats:sec>","DOI":"10.1093\/bioinformatics\/btw457","type":"journal-article","created":{"date-parts":[[2016,9,1]],"date-time":"2016-09-01T07:53:39Z","timestamp":1472716419000},"page":"i772-i780","source":"Crossref","is-referenced-by-count":38,"title":["Logical model specification aided by model-checking techniques: application to the mammalian cell cycle regulation"],"prefix":"10.1093","volume":"32","author":[{"given":"Pauline","family":"Traynard","sequence":"first","affiliation":[{"name":"Computational Systems Biology Team, Institut de Biologie de L\u2019Ecole Normale Sup\u00e9rieure (IBENS), CNRS, Inserm, Ecole Normale Sup\u00e9rieure, PSL Research University, Paris, France"},{"name":"EPI Lifeware, Inria Inria Saclay Ile-de-France, Palaiseau, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Adrien","family":"Faur\u00e9","sequence":"additional","affiliation":[{"name":"Graduate School of Science and Engineering, Yamaguchi University, Yamaguchi, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fran\u00e7ois","family":"Fages","sequence":"additional","affiliation":[{"name":"EPI Lifeware, Inria Inria Saclay Ile-de-France, Palaiseau, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Denis","family":"Thieffry","sequence":"additional","affiliation":[{"name":"Computational Systems Biology Team, Institut de Biologie de L\u2019Ecole Normale Sup\u00e9rieure (IBENS), CNRS, Inserm, Ecole Normale Sup\u00e9rieure, PSL Research University, Paris, France"},{"name":"EPI Lifeware, Inria Inria Saclay Ile-de-France, Palaiseau, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"286","published-online":{"date-parts":[[2016,8,29]]},"reference":[{"key":"2023020113393798700_btw457-B1","first-page":"86","article-title":"Model checking to assess T-helper cell plasticity","volume":"2","author":"Abou-Jaoud\u00e9","year":"2015","journal-title":"Front. Bioeng. Biotechnol"},{"key":"2023020113393798700_btw457-B2","doi-asserted-by":"crossref","first-page":"94","DOI":"10.3389\/fgene.2016.00094","article-title":"Logical modeling and dynamical analysis of cellular networks","volume":"7","author":"Abou-Jaoud\u00e9","year":"2016","journal-title":"Front. Genet"},{"key":"2023020113393798700_btw457-B3","doi-asserted-by":"crossref","first-page":"490.","DOI":"10.1186\/1471-2105-12-490","article-title":"Antelope: a hybrid-logic model checker for branching-time Boolean GRN analysis","volume":"12","author":"Arellano","year":"2011","journal-title":"BMC Bioinformatics"},{"key":"2023020113393798700_btw457-B4","doi-asserted-by":"crossref","first-page":"24","DOI":"10.4161\/cc.7.1.5232","article-title":"A reciprocal relationship between Rb and Skp2: implications for restriction point control, signal transduction to the cell cycle and cancer","volume":"7","author":"Assoian","year":"2008","journal-title":"Cell Cycle"},{"key":"2023020113393798700_btw457-B5","doi-asserted-by":"crossref","first-page":"i19","DOI":"10.1093\/bioinformatics\/bti1048","article-title":"Validation of qualitative models of genetic regulatory networks by model checking: analysis of the nutritional stress response in Escherichia coli","volume":"21","author":"Batt","year":"2005","journal-title":"Bioinformatics"},{"key":"2023020113393798700_btw457-B6","doi-asserted-by":"crossref","first-page":"i603","DOI":"10.1093\/bioinformatics\/btq387","article-title":"Efficient parameter search for qualitative models of regulatory networks using symbolic model checking","volume":"26","author":"Batt","year":"2010","journal-title":"Bioinformatics"},{"key":"2023020113393798700_btw457-B7","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1038\/ncb1532","article-title":"Retinoblastoma protein and anaphase-promoting complex physically interact and functionally cooperate during cell-cycle exit","volume":"9","author":"Binn\u00e9","year":"2007","journal-title":"Nat. Cell Biol"},{"key":"2023020113393798700_btw457-B8","doi-asserted-by":"crossref","first-page":"S85","DOI":"10.1098\/rsif.2008.0132.focus","article-title":"Boolean network models of cellular regulation: prospects and limitations","volume":"5","author":"Bornholdt","year":"2008","journal-title":"J. R. Soc. Interface"},{"key":"2023020113393798700_btw457-B9","author":"Chabrier","year":"2003"},{"key":"2023020113393798700_btw457-B10","doi-asserted-by":"crossref","first-page":"463","DOI":"10.1007\/978-1-61779-361-5_23","article-title":"Logical modelling of gene regulatory networks with ginsim","volume":"804","author":"Chaouiya","year":"2012","journal-title":"Methods Mol. Biol"},{"key":"2023020113393798700_btw457-B11","author":"Cimatti","year":"2002"},{"key":"2023020113393798700_btw457-B12","volume-title":"Model Checking","author":"Clarke","year":"1999"},{"key":"2023020113393798700_btw457-B13","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1016\/j.canlet.2013.01.025","article-title":"A novel CyclinE\/CyclinA-CDK Inhibitor targets p27Kip1 degradation, cell cycle progression and cell survival: Implications in cancer therapy","volume":"333","author":"Dai","year":"2013","journal-title":"Cancer Lett"},{"key":"2023020113393798700_btw457-B14","doi-asserted-by":"crossref","first-page":"21957.","DOI":"10.1038\/srep21957","article-title":"Principles of dynamical modularity in biological regulatory networks","volume":"16","author":"Deritei","year":"2016","journal-title":"Sci. Rep"},{"key":"2023020113393798700_btw457-B15","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1038\/nrm3567","article-title":"Molecular mechanisms underlying RB protein function","volume":"14","author":"Dick","year":"2013","journal-title":"Nat. Rev. Mol. Cell Biol"},{"key":"2023020113393798700_btw457-B16","doi-asserted-by":"crossref","first-page":"e124","DOI":"10.1093\/bioinformatics\/btl210","article-title":"Dynamical analysis of a generic Boolean model for the control of the mammalian cell cycle","volume":"22","author":"Faur\u00e9","year":"2006","journal-title":"Bioinformatics"},{"key":"2023020113393798700_btw457-B17","doi-asserted-by":"crossref","first-page":"1787","DOI":"10.1039\/b910101m","article-title":"Modular logical modelling of the budding yeast cell cycle","volume":"5","author":"Faur\u00e9","year":"2009","journal-title":"Mol. Biosyst"},{"key":"2023020113393798700_btw457-B18","doi-asserted-by":"crossref","first-page":"874","DOI":"10.1016\/j.cell.2011.03.006","article-title":"Modeling the cell cycle: why do certain circuits oscillate?","volume":"144","author":"Ferrell","year":"2011","journal-title":"Cell"},{"key":"2023020113393798700_btw457-B19","doi-asserted-by":"crossref","first-page":"e1004426.","DOI":"10.1371\/journal.pcbi.1004426","article-title":"Discovery of drug synergies in gastric cancer cells predicted by logical modeling","volume":"11","author":"Flobak","year":"2015","journal-title":"PLoS Comput. Biol"},{"key":"2023020113393798700_btw457-B20","doi-asserted-by":"crossref","first-page":"e69008.","DOI":"10.1371\/journal.pone.0069008","article-title":"Boolean network model for cancer pathways: predicting carcinogenesis and targeted therapy outcomes","volume":"8","author":"Fumia","year":"2013","journal-title":"PLoS ONE"},{"key":"2023020113393798700_btw457-B21","doi-asserted-by":"crossref","first-page":"431","DOI":"10.1016\/S0092-8674(03)00645-7","article-title":"Cyclin E ablation in the mouse","volume":"114","author":"Geng","year":"2003","journal-title":"Cell"},{"key":"2023020113393798700_btw457-B22","first-page":"21643","article-title":"Temporal self-organization of the cyclin\/cdk network driving the mammalian cell cycle","volume":"106","author":"G\u00e9rard","year":"2009","journal-title":"PLoS Comput. Biol"},{"key":"2023020113393798700_btw457-B23","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1016\/0022-5193(73)90208-7","article-title":"The logical analysis of continuous, non-linear biochemical control networks","volume":"39","author":"Glass","year":"1973","journal-title":"J. Theor. Biol"},{"key":"2023020113393798700_btw457-B24","doi-asserted-by":"crossref","first-page":"e1003286.","DOI":"10.1371\/journal.pcbi.1003286","article-title":"Integrative modelling of the influence of MAPK network on cancer cell fate decision","volume":"9","author":"Grieco","year":"2013","journal-title":"PLoS Comput. Biol"},{"key":"2023020113393798700_btw457-B25","doi-asserted-by":"crossref","first-page":"10.","DOI":"10.1186\/1747-1028-7-10","article-title":"The retinoblastoma family of proteins and their regulatory functions in the mammalian cell division cycle","volume":"7","author":"Henley","year":"2012","journal-title":"Cell Div"},{"key":"2023020113393798700_btw457-B26","doi-asserted-by":"crossref","first-page":"543","DOI":"10.1016\/j.jtbi.2008.12.028","article-title":"Logical analysis of the budding yeast cell cycle","volume":"257","author":"Irons","year":"2009","journal-title":"J. Theor. Biol"},{"key":"2023020113393798700_btw457-B27","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1016\/j.molcel.2004.09.029","article-title":"An Rb-Skp2-p27 pathway mediates acute cell cycle inhibition by Rb and is retained in a partial-penetrance Rb mutant","volume":"16","author":"Ji","year":"2004","journal-title":"Mol. Cell"},{"key":"2023020113393798700_btw457-B28","doi-asserted-by":"crossref","first-page":"2703","DOI":"10.1091\/mbc.10.8.2703","article-title":"Molecular interaction map of the mammalian cell cycle control and DNA repair systems","volume":"10","author":"Kohn","year":"1999","journal-title":"Mol. Biol. Cell"},{"key":"2023020113393798700_btw457-B29","doi-asserted-by":"crossref","first-page":"17694","DOI":"10.1074\/jbc.M500866200","article-title":"Molecular dissection of the interaction between p27 and Kip1 ubiquitylation-promoting complex, the ubiquitin ligase that regulates proteolysis of p27 in G1 phase","volume":"280","author":"Kotoshibai","year":"2005","journal-title":"J. Biol. Chem"},{"key":"2023020113393798700_btw457-B30","doi-asserted-by":"crossref","first-page":"436","DOI":"10.1016\/j.bbamcr.2013.11.005","article-title":"p27 is regulated independently of Skp2 in the absence of Cdk2","volume":"1843","author":"Kotoshiba","year":"2014","journal-title":"Biochim. Biophys. Acta"},{"key":"2023020113393798700_btw457-B31","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1016\/0092-8674(94)90582-7","article-title":"Negative regulation of the growth- promoting transcription factor E2F-1 by a stably bound cyclin A-dependent protein kinase","volume":"78","author":"Krek","year":"1994","journal-title":"Cell"},{"key":"2023020113393798700_btw457-B32","doi-asserted-by":"crossref","first-page":"1874","DOI":"10.1101\/gad.6.10.1874","article-title":"Cyclin E\/cdk2 and cyclin A\/cdk2 kinases associate with p107 and E2F in a temporally distinct manner","volume":"66","author":"Lees","year":"1992","journal-title":"Genes Dev"},{"key":"2023020113393798700_btw457-B33","doi-asserted-by":"crossref","first-page":"4781","DOI":"10.1073\/pnas.0305937101","article-title":"The yeast cell-cycle network is robustly designed","volume":"101","author":"Li","year":"2004","journal-title":"Proc. Natl. Acad. Sci. U. S. A"},{"key":"2023020113393798700_btw457-B34","doi-asserted-by":"crossref","first-page":"9015","DOI":"10.1158\/0008-5472.CAN-08-1935","article-title":"Imatinib mesylate induces quiescence in gastrointestinal stromal tumor cells through the CDH1-SKP2-p27Kip1 signaling axis","volume":"68","author":"Liu","year":"2008","journal-title":"Cancer Res"},{"key":"2023020113393798700_btw457-B35","doi-asserted-by":"crossref","first-page":"753","DOI":"10.1128\/MCB.18.2.753","article-title":"Functional inactivation of the retinoblastoma protein requires sequential modification by at least two distinct cyclin-cdk complexes","volume":"18","author":"Lundberg","year":"1998","journal-title":"Mol. Cell. Biol"},{"key":"2023020113393798700_btw457-B36","doi-asserted-by":"crossref","first-page":"544","DOI":"10.1016\/j.semcdb.2011.03.009","article-title":"Processive ubiquitin chain formation by the anaphase-promoting complex","volume":"22","author":"Meyer","year":"2011","journal-title":"Semin. Cell Dev. Biol"},{"key":"2023020113393798700_btw457-B37","doi-asserted-by":"crossref","first-page":"S7.","DOI":"10.1186\/1471-2164-15-S7-S7","article-title":"Modelling the onset of senescence at the g1\/s cell cycle checkpoint","volume":"15","author":"Mombach","year":"2014","journal-title":"BMC Genomics"},{"key":"2023020113393798700_btw457-B38","doi-asserted-by":"crossref","first-page":"1181","DOI":"10.1101\/gad.13.9.1181","article-title":"Ubiquitination of p27 is regulated by CDK dependent phosphorylation and trimeric comples formation","volume":"13","author":"Montagnoli","year":"1999","journal-title":"Genes Dev"},{"key":"2023020113393798700_btw457-B39","doi-asserted-by":"crossref","first-page":"2069","DOI":"10.1093\/emboj\/19.9.2069","article-title":"Targeted disruption of Skp2 results in accumulation of cyclin E and p27(Kip1), polyploidy and centrosome overduplication","volume":"19","author":"Nakayama","year":"2000","journal-title":"Embo J"},{"key":"2023020113393798700_btw457-B40","doi-asserted-by":"crossref","first-page":"661","DOI":"10.1016\/S1534-5807(04)00131-5","article-title":"Skp2-Mediated degradation of p27 regulates progression into mitosis","volume":"6","author":"Nakayama","year":"2004","journal-title":"Dev. Cell"},{"key":"2023020113393798700_btw457-B41","doi-asserted-by":"crossref","first-page":"e02872.","DOI":"10.7554\/eLife.02872","article-title":"Cyclin D activates the Rb tumor suppressor by mono-phosphorylation","volume":"3","author":"Narasimha","year":"2014","journal-title":"eLife"},{"key":"2023020113393798700_btw457-B42","doi-asserted-by":"crossref","first-page":"4528","DOI":"10.1074\/jbc.272.7.4528","article-title":"High molecular weight protein phosphatase type 1 dephosphorylates the retinoblastoma protein","volume":"272","author":"Nelson","year":"1997","journal-title":"J. Biol. Chem"},{"key":"2023020113393798700_btw457-B43","doi-asserted-by":"crossref","first-page":"1383","DOI":"10.1016\/j.jtbi.2004.04.039","article-title":"A model for restriction point control of the mammalian cell cycle","volume":"230","author":"Nov\u00e1k","year":"2004","journal-title":"J. Theor. Biol"},{"key":"2023020113393798700_btw457-B44","doi-asserted-by":"crossref","first-page":"2612","DOI":"10.1128\/MCB.15.5.2612","article-title":"Human cyclin E, a nuclear protein essential for the G1-to-S phase transition","volume":"15","author":"Ohtsubo","year":"1995","journal-title":"Mol. Cell. Biol"},{"key":"2023020113393798700_btw457-B45","doi-asserted-by":"crossref","first-page":"3956","DOI":"10.4161\/cc.9.19.13162","article-title":"APC\/C(Cdc20) targets E2F1 for degradation in prometaphase","volume":"9","author":"Peart","year":"2010","journal-title":"Cell Cycle"},{"key":"2023020113393798700_btw457-B46","doi-asserted-by":"crossref","first-page":"588","DOI":"10.1038\/nature03023","article-title":"Autonomous regulation of the anaphase-promoting complex couples mitosis to S-phase entry","volume":"432","author":"Rape","year":"2004","journal-title":"Nature"},{"key":"2023020113393798700_btw457-B47","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1016\/j.cell.2005.10.032","article-title":"The processivity of multiubiquitination by the APC determines the order of substrate degradation","volume":"124","author":"Rape","year":"2006","journal-title":"Cell"},{"key":"2023020113393798700_btw457-B48","doi-asserted-by":"crossref","first-page":"4042","DOI":"10.1158\/0008-5472.CAN-15-0602","article-title":"A modeling approach to explain mutually exclusive and co-occurring genetic alterations in bladder tumorigenesis","volume":"75","author":"Remy","year":"2015","journal-title":"Cancer Res"},{"key":"2023020113393798700_btw457-B49","doi-asserted-by":"crossref","first-page":"18337","DOI":"10.1074\/jbc.271.31.18337","article-title":"Abrogation of p27Kip1 by cDNA antisense suppresses quiescence (G0 state) in fibroblasts","volume":"271","author":"Rivard","year":"1996","journal-title":"J. Biol. Chem"},{"key":"2023020113393798700_btw457-B50","doi-asserted-by":"crossref","first-page":"116.","DOI":"10.1186\/1752-0509-6-116","article-title":"Continuous time Boolean modeling for biological signaling: application of gillespie algorithm","volume":"6","author":"Stoll","year":"2012","journal-title":"BMC Syst. Biol"},{"key":"2023020113393798700_btw457-B51","doi-asserted-by":"crossref","first-page":"563","DOI":"10.1016\/0022-5193(73)90247-6","article-title":"Boolean formalization of genetic control circuits","volume":"42","author":"Thomas","year":"1973","journal-title":"J. Theor. Biol"},{"key":"2023020113393798700_btw457-B52","doi-asserted-by":"crossref","first-page":"2362","DOI":"10.1073\/pnas.94.6.2362","article-title":"Dominant-negative cyclin-selective ubiquitin carrier protein E2-C\/UbcH10 blocks cells in metaphase","volume":"94","author":"Townsley","year":"1997","journal-title":"Proc. Natl. Acad. Sci. U. S. A"},{"key":"2023020113393798700_btw457-B53","doi-asserted-by":"crossref","first-page":"46.","DOI":"10.1186\/s12915-015-0158-9","article-title":"Models in biology: lessons from modeling regulation of the eukaryotic cell cycle","volume":"13","author":"Tyson","year":"2015","journal-title":"BMC Biol"},{"key":"2023020113393798700_btw457-B54","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1016\/0092-8674(95)90385-2","article-title":"The retinoblastoma protein and cell cycle control","volume":"81","author":"Weinberg","year":"1995","journal-title":"Cell"},{"key":"2023020113393798700_btw457-B55","doi-asserted-by":"crossref","first-page":"1\u201313.","DOI":"10.1371\/journal.pone.0097130","article-title":"A data-driven, mathematical model of mammalian cell cycle regulation","volume":"9","author":"Weis","year":"2014","journal-title":"PLoS ONE"},{"key":"2023020113393798700_btw457-B56","doi-asserted-by":"crossref","first-page":"3086","DOI":"10.4161\/cc.10.18.17350","article-title":"Control of E2F dynamics in cell cycle entry","volume":"10","author":"Wong","year":"2014","journal-title":"Cell Cycle"}],"container-title":["Bioinformatics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/academic.oup.com\/bioinformatics\/article-pdf\/32\/17\/i772\/49021601\/bioinformatics_32_17_i772.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/academic.oup.com\/bioinformatics\/article-pdf\/32\/17\/i772\/49021601\/bioinformatics_32_17_i772.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,1]],"date-time":"2023-02-01T23:45:22Z","timestamp":1675295122000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/bioinformatics\/article\/32\/17\/i772\/2450787"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,8,29]]},"references-count":56,"journal-issue":{"issue":"17","published-print":{"date-parts":[[2016,9,1]]}},"URL":"https:\/\/doi.org\/10.1093\/bioinformatics\/btw457","relation":{},"ISSN":["1367-4803","1367-4811"],"issn-type":[{"value":"1367-4803","type":"print"},{"value":"1367-4811","type":"electronic"}],"subject":[],"published-other":{"date-parts":[[2016,9,1]]},"published":{"date-parts":[[2016,8,29]]}}}