{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,20]],"date-time":"2026-01-20T11:07:22Z","timestamp":1768907242689,"version":"3.49.0"},"reference-count":76,"publisher":"Springer Science and Business Media LLC","issue":"1","content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["BMC Bioinformatics"],"published-print":{"date-parts":[[2011,12]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:sec>\n            <jats:title>Background<\/jats:title>\n            <jats:p>In Thomas' formalism for modeling gene regulatory networks (GRNs), <jats:italic>branching time<\/jats:italic>, where a state can have <jats:italic>more than one possible future<\/jats:italic>, plays a prominent role. By representing a certain degree of unpredictability, branching time can model several important phenomena, such as (a) asynchrony, (b) incompletely specified behavior, and (c) interaction with the environment. Introducing more than one possible future for a state, however, creates a difficulty for ordinary simulators, because <jats:italic>infinitely many<\/jats:italic> paths may appear, limiting ordinary simulators to statistical conclusions. <jats:italic>Model checkers<\/jats:italic> for branching time, by contrast, are able to prove properties in the presence of infinitely many paths.<\/jats:p>\n          <\/jats:sec>\n          <jats:sec>\n            <jats:title>Results<\/jats:title>\n            <jats:p>We have developed <jats:italic>Antelope<\/jats:italic> (\"Analysis of Networks through TEmporal-LOgic sPEcifications\", <jats:ext-link xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" xlink:href=\"http:\/\/turing.iimas.unam.mx:8080\/AntelopeWEB\/\" ext-link-type=\"uri\">http:\/\/turing.iimas.unam.mx:8080\/AntelopeWEB\/<\/jats:ext-link>), a model checker for analyzing and constructing Boolean GRNs. Currently, software systems for Boolean GRNs use branching time almost exclusively for asynchrony. <jats:italic>Antelope<\/jats:italic>, by contrast, also uses branching time for incompletely specified behavior and environment interaction. We show the usefulness of modeling these two phenomena in the development of a Boolean GRN of the <jats:italic>Arabidopsis thaliana<\/jats:italic> root stem cell niche.<\/jats:p>\n            <jats:p>There are two obstacles to a direct approach when applying model checking to Boolean GRN analysis. First, ordinary model checkers normally only verify whether or not a <jats:italic>given<\/jats:italic> set of model states has a given property. In comparison, a model checker for Boolean GRNs is preferable if it <jats:italic>reports<\/jats:italic> the set of states having a desired property. Second, for efficiency, the expressiveness of many model checkers is limited, resulting in the inability to express some interesting properties of Boolean GRNs.<\/jats:p>\n            <jats:p>\n              <jats:italic>Antelope<\/jats:italic> tries to overcome these two drawbacks: Apart from reporting the set of all states having a given property, our model checker can express, at the expense of efficiency, some properties that ordinary model checkers (e.g., NuSMV) cannot. This additional expressiveness is achieved by employing a logic extending the standard Computation-Tree Logic (CTL) with hybrid-logic operators.<\/jats:p>\n          <\/jats:sec>\n          <jats:sec>\n            <jats:title>Conclusions<\/jats:title>\n            <jats:p>We illustrate the advantages of <jats:italic>Antelope<\/jats:italic> when (a) modeling incomplete networks and environment interaction, (b) exhibiting the set of all states having a given property, and (c) representing Boolean GRN properties with hybrid CTL.<\/jats:p>\n          <\/jats:sec>","DOI":"10.1186\/1471-2105-12-490","type":"journal-article","created":{"date-parts":[[2011,12,22]],"date-time":"2011-12-22T19:26:25Z","timestamp":1324581985000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":32,"title":["\"Antelope\": a hybrid-logic model checker for branching-time Boolean GRN analysis"],"prefix":"10.1186","volume":"12","author":[{"given":"Gustavo","family":"Arellano","sequence":"first","affiliation":[]},{"given":"Juli\u00e1n","family":"Argil","sequence":"additional","affiliation":[]},{"given":"Eugenio","family":"Azpeitia","sequence":"additional","affiliation":[]},{"given":"Mariana","family":"Ben\u00edtez","sequence":"additional","affiliation":[]},{"given":"Miguel","family":"Carrillo","sequence":"additional","affiliation":[]},{"given":"Pedro","family":"G\u00f3ngora","sequence":"additional","affiliation":[]},{"given":"David A","family":"Rosenblueth","sequence":"additional","affiliation":[]},{"given":"Elena R","family":"Alvarez-Buylla","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2011,12,22]]},"reference":[{"key":"5125_CR1","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1038\/35018085","volume":"406","author":"G von Dassow","year":"2000","unstructured":"von Dassow G, Meir E, Munro E, Odell G: The segment polarity network is a robust developmental module. Nature 2000, 406: 188\u2013192. 10.1038\/35018085","journal-title":"Nature"},{"key":"5125_CR2","doi-asserted-by":"publisher","first-page":"2923","DOI":"10.1105\/tpc.104.021725","volume":"16","author":"C Espinosa-Soto","year":"2004","unstructured":"Espinosa-Soto C, Padilla-Longoria P, Alvarez-Buylla E: A gene regulatory network model for cell-fate determination during Arabidopsis thaliana flower development that is robust and recovers experimental gene expression profiles. The Plant Cell 2004, 16: 2923\u20132939. 10.1105\/tpc.104.021725","journal-title":"The Plant Cell"},{"issue":"10","key":"5125_CR3","doi-asserted-by":"publisher","first-page":"1732","DOI":"10.1371\/journal.pbio.0040312","volume":"4","author":"S Li","year":"2006","unstructured":"Li S, Assmann SM, Albert R: Predicting essential components of signal transduction networks: a dynamic model of guard cell abscisic acid signaling. PLoS Biology 2006, 4(10):1732\u20131748.","journal-title":"PLoS Biology"},{"key":"5125_CR4","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1007\/978-3-540-44485-5_21","volume-title":"Complex Networks","author":"R Albert","year":"2004","unstructured":"Albert R: Boolean modeling of genetic regulatory networks. In Complex Networks. Edited by: Ben-Naim E, Frauenfelder H, Toroczkai Z. Springer; 2004:459\u2013481. [Lecture Notes in Physics Vol. 650]"},{"key":"5125_CR5","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1089\/10665270252833208","volume":"9","author":"H de Jong","year":"2002","unstructured":"de Jong H: Modeling and simulation of genetic regulatory systems: a literature review. Journal of Computational Biology 2002, 9: 67\u2013103. 10.1089\/10665270252833208","journal-title":"Journal of Computational Biology"},{"issue":"11","key":"5125_CR6","doi-asserted-by":"publisher","first-page":"1239","DOI":"10.1038\/nbt1356","volume":"25","author":"J Fisher","year":"2007","unstructured":"Fisher J, Henzinger TA: Executable cell biology. Nature Biotechnology 2007, 25(11):1239\u20131249. 10.1038\/nbt1356","journal-title":"Nature Biotechnology"},{"key":"5125_CR7","doi-asserted-by":"publisher","first-page":"S85","DOI":"10.1098\/rsif.2008.0132.focus","volume":"5","author":"S Bornholdt","year":"2008","unstructured":"Bornholdt S: Boolean network models of cellular regulation: prospects and limitations. J R Soc Interface 2008, 5: S85-S94. 10.1098\/rsif.2008.0132.focus","journal-title":"J R Soc Interface"},{"key":"5125_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0022-5193(03)00035-3","volume":"223","author":"R Albert","year":"2003","unstructured":"Albert R, Othmer HG: The topology of the regulatory interactions predicts the expression pattern of the segment polarity genes in Drosophila melanogaster. J Theor Biol 2003, 223: 1\u201318. 10.1016\/S0022-5193(03)00035-3","journal-title":"J Theor Biol"},{"key":"5125_CR9","doi-asserted-by":"publisher","first-page":"e0999","DOI":"10.1199\/tab.0127","volume":"8","author":"ER Alvarez-Buylla","year":"2010","unstructured":"Alvarez-Buylla ER, Ben\u00edtez M, Corvera-Poir\u00e9 A, Candor AC, de Folter S, de Buen AG, Garay-Arroyo A, Garc\u00eda-Ponce B, Jaimes-Miranda F, P\u00e9rez-Ruiz RV, Pineiro-Nelson A, S\u00e1nchez-Corrales YE: Flower development. The Arabidopsis Book 2010, 8: e0999. [Doi:10.1199\/tab.0999] [Doi:10.1199\/tab.0999]","journal-title":"The Arabidopsis Book"},{"issue":"14","key":"5125_CR10","doi-asserted-by":"publisher","first-page":"e124","DOI":"10.1093\/bioinformatics\/btl210","volume":"22","author":"A Faur\u00e9","year":"2006","unstructured":"Faur\u00e9 A, Naldi A, Chaouiya C, Thieffry D: Dynamical analysis of a genetic Boolean model for the control of the mammalian cell cycle. Bioinformatics 2006, 22(14):e124-e131. 10.1093\/bioinformatics\/btl210","journal-title":"Bioinformatics"},{"issue":"14","key":"5125_CR11","doi-asserted-by":"publisher","first-page":"4781","DOI":"10.1073\/pnas.0305937101","volume":"101","author":"F Li","year":"2004","unstructured":"Li F, Long T, Lu Y, Ouyang Q, Tang C: The yeast cell-cycle network is robustly designed. Proc Natl Acad Sci USA 2004, 101(14):4781\u20134786. 10.1073\/pnas.0305937101","journal-title":"Proc Natl Acad Sci USA"},{"issue":"2","key":"5125_CR12","doi-asserted-by":"publisher","first-page":"e1672","DOI":"10.1371\/journal.pone.0001672","volume":"3","author":"MI Davidich","year":"2008","unstructured":"Davidich MI, Bornholdt S: Boolean network model predicts cell cycle sequence of fission yeast. PLoS One 2008, 3(2):e1672. [Doi:10.1371\/journal.pone.0001672] [Doi:10.1371\/journal.pone.0001672] 10.1371\/journal.pone.0001672","journal-title":"PLoS One"},{"key":"5125_CR13","volume-title":"Biological Feedback","author":"R Thomas","year":"1990","unstructured":"Thomas R, D'Ari R: Biological Feedback. CRC Press; 1990."},{"key":"5125_CR14","first-page":"1","volume-title":"J Theor Biol","author":"R Thomas","year":"1991","unstructured":"Thomas R: Regulatory networks seen as asynchronous automata. J Theor Biol 1991, 1\u201323."},{"issue":"2","key":"5125_CR15","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/BF02460618","volume":"57","author":"R Thomas","year":"1995","unstructured":"Thomas R, Thieffry D, Kaufman M: Dynamical behaviour of biological regulatory networks--I. Biological role of feedback loops and practical use of the concept of the loop-characteristic state. Bull Math Biol 1995, 57(2):247\u2013276.","journal-title":"Bull Math Biol"},{"key":"5125_CR16","volume-title":"Source Code Biol Med","author":"I Albert","year":"2008","unstructured":"Albert I, Thakar J, Li S, Zhang R, Albert R: Boolean networks simulations for life scientists. Source Code Biol Med 2008., 3(16): [Doi: 10.1186\/1751\u20130473\u20133-16]"},{"issue":"10","key":"5125_CR17","doi-asserted-by":"publisher","first-page":"1378","DOI":"10.1093\/bioinformatics\/btq124","volume":"26","author":"C M\u00fcssel","year":"2010","unstructured":"M\u00fcssel C, Hopfensitz M, Kestler HA: BoolNet--an R package for generation, reconstruction and analysis of Boolean networks. Bioinformatics 2010, 26(10):1378\u20131380. [Applications Note] [Applications Note] 10.1093\/bioinformatics\/btq124","journal-title":"Bioinformatics"},{"key":"5125_CR18","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/978-3-540-44928-7_17","volume":"294","author":"C Chaouiya","year":"2003","unstructured":"Chaouiya C, Remy E, Moss\u00e9 B, Thieffry D: Qualitative analysis of regulatory graphs: a computational tool based on a discrete formal framework. Positive Systems, LNCIS 2003, 294: 119\u2013126.","journal-title":"Positive Systems, LNCIS"},{"key":"5125_CR19","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1016\/j.biosystems.2005.10.003","volume":"84","author":"AG Gonzalez","year":"2006","unstructured":"Gonzalez AG, Naldia A, S\u00e1nchez L, Thieffry D, Chaouiya C: GINsim: A software suite for the qualitative modelling, simulation and analysis of regulatory networks. BioSystems 2006, 84: 91\u2013100. 10.1016\/j.biosystems.2005.10.003","journal-title":"BioSystems"},{"key":"5125_CR20","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1016\/j.biosystems.2009.04.008","volume":"97","author":"A Naldi","year":"2009","unstructured":"Naldi A, Berenguier D, Faur\u00e9 A, Lopez F, Thieffry D, Chaouiya C: Logical modelling of regulatory networks with GINsim 2.3. BioSystems 2009, 97: 134\u2013139. 10.1016\/j.biosystems.2009.04.008","journal-title":"BioSystems"},{"key":"5125_CR21","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1016\/j.biosystems.2009.07.007","volume":"98","author":"F Corblin","year":"2009","unstructured":"Corblin F, Tripodi S, Fanchon E, Ropers D, Trilling L: A declarative constraint-based method for analyzing discrete genetic regulatory networks. BioSystems 2009, 98: 91\u2013104. 10.1016\/j.biosystems.2009.07.007","journal-title":"BioSystems"},{"key":"5125_CR22","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1186\/1471-2105-11-385","volume":"11","author":"F Corblin","year":"2010","unstructured":"Corblin F, Fanchon E, Trilling L: Applications of a formal approach to decipher discrete genetic networks. BMC Bioinfomatics 2010, 11: 385. 10.1186\/1471-2105-11-385","journal-title":"BMC Bioinfomatics"},{"key":"5125_CR23","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1016\/j.jtbi.2004.04.003","volume":"229","author":"G Bernot","year":"2004","unstructured":"Bernot G, Comet JP, Richard A, Guespin J: Application of formal methods to biological regulatory networks: extending Thomas' asynchronous logical approach with temporal logic. Journal of Theoretical Biology 2004, 229: 339\u2013347. 10.1016\/j.jtbi.2004.04.003","journal-title":"Journal of Theoretical Biology"},{"key":"5125_CR24","first-page":"15","volume":"3","author":"Z Khalis","year":"2009","unstructured":"Khalis Z, Comet JP, Richard A, Bernot G: The SMBioNet method for discovering models of gene regulatory networks. Genes, Genomes and Genomics 2009, 3: 15\u201322.","journal-title":"Genes, Genomes and Genomics"},{"key":"5125_CR25","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1186\/1742-4682-3-13","volume":"3","author":"L Mendoza","year":"2006","unstructured":"Mendoza L, Xenarios I: A method for the generation of standardized qualitative dynamical systems of regulatory networks. Theoretical Biology and Medical Modelling 2006, 3: 13. 10.1186\/1742-4682-3-13","journal-title":"Theoretical Biology and Medical Modelling"},{"key":"5125_CR26","doi-asserted-by":"publisher","first-page":"462","DOI":"10.1186\/1471-2105-8-462","volume":"8","author":"AD Cara","year":"2007","unstructured":"Cara AD, Garg A, Micheli BD, Xenarios I, Mendoza L: Dynamic simulation of regulatory networks using SQUAD. BMC Bioinformatics 2007, 8: 462. 10.1186\/1471-2105-8-462","journal-title":"BMC Bioinformatics"},{"key":"5125_CR27","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/978-3-540-71681-5_5","volume-title":"Proc Research in Computational Molecular Biology","author":"A Garg","year":"2007","unstructured":"Garg A, Xenarios I, Mendoza L, DeMicheli G: An efficient method for dynamic analysis of gene regulatory networks and in silico gene perturbation experiments. Proc Research in Computational Molecular Biology 2007, 62\u201376. [Lecture Notes in Computer Science No. 4453] [Lecture Notes in Computer Science No. 4453]"},{"key":"5125_CR28","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1259\/bjr\/64628752","volume":"27","author":"LE Feinendegen","year":"2005","unstructured":"Feinendegen LE: Significance of basic and clinical research in radiation medicine: challenges for the future. British Institute of Radiology supplement 2005, 27: 185\u2013195.","journal-title":"British Institute of Radiology supplement"},{"key":"5125_CR29","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511794797","volume-title":"Artificial Intelligence. Foundations of Computational Agents","author":"DL Poole","year":"2010","unstructured":"Poole DL, Mackworth AK: Artificial Intelligence. Foundations of Computational Agents. Cambridge University Press; 2010."},{"issue":"7","key":"5125_CR30","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1145\/79204.79209","volume":"33","author":"J Cohen","year":"1990","unstructured":"Cohen J: Constraint logic programming languages. Communications of the ACM 1990, 33(7):52\u201368. 10.1145\/79204.79209","journal-title":"Communications of the ACM"},{"key":"5125_CR31","first-page":"52","volume-title":"Proc Workshop on Logics of Programs","author":"EM Clarke","year":"1981","unstructured":"Clarke EM, Emerson EA: Design and synthesis of synchronization skeletons using branching time temporal logic. In Proc Workshop on Logics of Programs. IBM Watson Research Center; 1981:52\u201371. [Lecture Notes in Computer Science No. 131] [Lecture Notes in Computer Science No. 131]"},{"key":"5125_CR32","first-page":"337","volume-title":"Proc 5th International Symposium on Programming","author":"JP Quielle","year":"1981","unstructured":"Quielle JP, Sifakis J: Specification and verification of concurrent systems in CESAR. Proc 5th International Symposium on Programming 1981, 337\u2013350."},{"key":"5125_CR33","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/978-3-540-69850-0_2","volume-title":"25 Years of Model Checking","author":"EA Emerson","year":"2008","unstructured":"Emerson EA: The beginning of model checking: a personal perspective. In 25 Years of Model Checking. Springer; 2008:27\u201345. [Lecture Notes in Computer Science No. 5000, DOI: 10.1007\/978-3-540-69850-0_2]"},{"key":"5125_CR34","first-page":"400","volume-title":"Proc Pacific Symposium on Biocomputing","author":"S Eker","year":"2002","unstructured":"Eker S, Knapp M, Laderoute K, Lincoln P, Meseguer J, Sonmez K: Pathway logic: symbolic analysis of biological signaling. Proc Pacific Symposium on Biocomputing 2002, 400\u2013412."},{"key":"5125_CR35","first-page":"179","volume-title":"Proc Computational Methods in Systems Biology","author":"M Calder","year":"2005","unstructured":"Calder M, Vyshemirsky V, Gilbert D, Orton R: Analysis of signalling pathways using the PRISM model checker. Proc Computational Methods in Systems Biology 2005, 179\u2013190. [Lecture Notes in Computer Science No. 4416] [Lecture Notes in Computer Science No. 4416]"},{"key":"5125_CR36","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1159\/000110010","volume":"3","author":"J Ahmad","year":"2006","unstructured":"Ahmad J, Bernot G, Comet JP, Lime D, Roux O: Hybrid modelling and dynamical analysis of gene regulatory networks with delays. Complexus 2006, 3: 231\u2013251. 10.1159\/000110010","journal-title":"Complexus"},{"issue":"3","key":"5125_CR37","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1016\/j.tcs.2007.11.013","volume":"391","author":"J Heath","year":"2008","unstructured":"Heath J, Kwiatkowska M, Norman G, Parker D, Tymchyshyn O: Probabilistic model checking of complex biological pathways. Theoretical Computer Science 2008, 391(3):239\u2013257. 10.1016\/j.tcs.2007.11.013","journal-title":"Theoretical Computer Science"},{"key":"5125_CR38","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1016\/j.entcs.2009.02.048","volume":"232","author":"F Ciocchetta","year":"2009","unstructured":"Ciocchetta F, Gilmore S, Guerriero ML, Hillston J: Integrated simulation and model-checking for the analysis of biochemical systems. Electronic Notes in Theoretical Computer Science 2009, 232: 17\u201338.","journal-title":"Electronic Notes in Theoretical Computer Science"},{"issue":"2b","key":"5125_CR39","doi-asserted-by":"publisher","first-page":"627","DOI":"10.1142\/S0219720007002850","volume":"5","author":"D Mateus","year":"2007","unstructured":"Mateus D, Gallois JP, Comet JP, Gall PL: Symbolic modeling of genetic regulatory networks. Journal of Bioinformatics and Computational Biology 2007, 5(2b):627\u2013640. 10.1142\/S0219720007002850","journal-title":"Journal of Bioinformatics and Computational Biology"},{"issue":"Suppl 1","key":"5125_CR40","doi-asserted-by":"publisher","first-page":"i19","DOI":"10.1093\/bioinformatics\/bti1048","volume":"21","author":"G Batt","year":"2005","unstructured":"Batt G, Ropers D, de Jong H, Geiselmann J, Mateescu R, Page M, Schneider D: Validation of qualitative models of genetic regulatory networks by model checking: analysis of the nutritional stress response in Escherichia coli . Bioinformatics 2005, 21(Suppl 1):i19-i28. 10.1093\/bioinformatics\/bti1048","journal-title":"Bioinformatics"},{"issue":"14","key":"5125_CR41","doi-asserted-by":"publisher","first-page":"1805","DOI":"10.1093\/bioinformatics\/btl172","volume":"22","author":"L Calzone","year":"2006","unstructured":"Calzone L, Fages F, Soliman S: BIOCHAM: An environment for modeling biological systems and formalizing experimental knowledge. Bioinformatics 2006, 22(14):1805\u20131807. 10.1093\/bioinformatics\/btl172","journal-title":"Bioinformatics"},{"key":"5125_CR42","doi-asserted-by":"crossref","unstructured":"Li C, Nagasaki M, Ueno K, Miyano S: Simulation-based model checking approach to cell fate specification during Caenorhabditis elegans vulval development by hybrid functional Petri net with extension. BMC Systems Biology 2009., 3(42): [Doi:10.1186\/1752\u20130509\u20133-42] [Doi:10.1186\/1752-0509-3-42]","DOI":"10.1186\/1752-0509-3-42"},{"issue":"5","key":"5125_CR43","doi-asserted-by":"publisher","first-page":"e92","DOI":"10.1371\/journal.pcbi.0030092","volume":"3","author":"J Fisher","year":"2007","unstructured":"Fisher J, Piterman N, Hajnal A, Henzinger TA: Predictive modeling of signaling crosstalk during C. elegans vulval development. PLoS Computational Biology 2007, 3(5):e92. [Doi:10.1371\/journal.pcbi.0030092] [Doi:10.1371\/journal.pcbi.0030092] 10.1371\/journal.pcbi.0030092","journal-title":"PLoS Computational Biology"},{"key":"5125_CR44","doi-asserted-by":"publisher","DOI":"10.1093\/acprof:oso\/9780198243113.001.0001","volume-title":"Past, Present and Future. Clarendon","author":"A Prior","year":"1967","unstructured":"Prior A: Past, Present and Future. Clarendon. 1967."},{"key":"5125_CR45","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/BF01049415","volume":"4","author":"P Blackburn","year":"1995","unstructured":"Blackburn P, Seligman J: Hybrid languages. Journal of Logic, Language and Information 1995, 4: 251\u2013272. 10.1007\/BF01049415","journal-title":"Journal of Logic, Language and Information"},{"issue":"2","key":"5125_CR46","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"EM Clarke","year":"1986","unstructured":"Clarke EM, Emerson EA, Sistla AP: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions of Programming Languages and Systems 1986, 8(2):244\u2013263. 10.1145\/5397.5399","journal-title":"ACM Transactions of Programming Languages and Systems"},{"key":"5125_CR47","volume-title":"Model Checking","author":"EM Clarke","year":"1999","unstructured":"Clarke EM, Grumberg O, Peled DA: Model Checking. MIT Press; 1999."},{"key":"5125_CR48","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-04558-9","volume-title":"Systems and Software Verification. Model-Checking Techniques and Tools","author":"B B\u00e9rard","year":"2001","unstructured":"B\u00e9rard B, Bidoit M, Finkel A, Laroussinie F, Petit A, Petrucci L, Schnoebelen P, McKenzie P: Systems and Software Verification. Model-Checking Techniques and Tools. Springer; 2001."},{"key":"5125_CR49","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511810275","volume-title":"Logic in Computer Science. Modelling and reasoning about systems","author":"MRA Huth","year":"2004","unstructured":"Huth MRA, Ryan MD: Logic in Computer Science. Modelling and reasoning about systems. 2nd edition. Cambridge University Press; 2004.","edition":"2"},{"key":"5125_CR50","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier C, Katoen JP: Principles of Model Checking. MIT Press; 2008."},{"key":"5125_CR51","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/j.tcs.2004.03.063","volume":"325","author":"N Chabrier-Rivier","year":"2004","unstructured":"Chabrier-Rivier N, Chiaverini M, Danos V, Fages F, Sch\u00e4chter V: Modeling and querying biomolecular interaction networks. Theoretical Computer Science 2004, 325: 25\u201344. 10.1016\/j.tcs.2004.03.063","journal-title":"Theoretical Computer Science"},{"issue":"3","key":"5125_CR52","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/j.jal.2005.06.010","volume":"4","author":"M Franceschet","year":"2006","unstructured":"Franceschet M, de Rijke M: Model checking hybrid logics (with an application to semistructured data). Journal of Applied Logic 2006, 4(3):279\u2013304. 10.1016\/j.jal.2005.06.010","journal-title":"Journal of Applied Logic"},{"key":"5125_CR53","first-page":"821","volume-title":"Handbook of Modal Logics","author":"C Areces","year":"2006","unstructured":"Areces C, ten Cate B: Hybrid logics. In Handbook of Modal Logics. Edited by: Blackburn P, Wolter F, van Benthem J. Elsevier; 2006:821\u2013868."},{"key":"5125_CR54","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J Burch","year":"1992","unstructured":"Burch J, Clarke E, McMillan K, Dill DL, Hwang LJ: Symbolic model checking: 1020states and beyond. Information and Computation 1992, 98: 142\u2013170. 10.1016\/0890-5401(92)90017-A","journal-title":"Information and Computation"},{"issue":"8","key":"5125_CR55","doi-asserted-by":"publisher","first-page":"1035","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"RE Bryant","year":"1986","unstructured":"Bryant RE: Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers 1986, C-35(8):1035\u20131044.","journal-title":"IEEE Transactions on Computers"},{"key":"5125_CR56","volume-title":"JavaBDD 1.0b2","author":"J Whaley","year":"2007","unstructured":"Whaley J: JavaBDD 1.0b2.2007. [http:\/\/javabdd.sourceforge.net\/]"},{"key":"5125_CR57","volume-title":"BuDDy 2.4","author":"J Lind-Nielsen","year":"2004","unstructured":"Lind-Nielsen J: BuDDy 2.4.2004. [http:\/\/sourceforge.net\/projects\/buddy\/]"},{"issue":"5","key":"5125_CR58","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1038\/nrm2164","volume":"8","author":"B Scheres","year":"2007","unstructured":"Scheres B: Stem-cell niches: nursery rhymes across kingdoms. Nat Rev Mol Cell Biol 2007, 8(5):345\u2013354. 10.1038\/nrm2164","journal-title":"Nat Rev Mol Cell Biol"},{"key":"5125_CR59","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1242\/dev.119.1.71","volume":"119","author":"L Dolan","year":"1993","unstructured":"Dolan L, Janmaat K, Willemsen V, Linstead P, Poethig S, Roberts K, Scheres B: Cellular organisation of the Arabidopsis thaliana root. Development 1993, 119: 71\u201384.","journal-title":"Development"},{"issue":"7137","key":"5125_CR60","doi-asserted-by":"publisher","first-page":"811","DOI":"10.1038\/nature05703","volume":"446","author":"AK Sarkar","year":"2007","unstructured":"Sarkar AK, Luijten M, Miyashima S, Lenhard M, Hashimoto T, Nakajima K, Scheres B, Heidstra R, Laux T: Conserved factors regulate signalling in Arabidopsis thaliana shoot and root stem cell organizers. Nature 2007, 446(7137):811\u2013814. 10.1038\/nature05703","journal-title":"Nature"},{"key":"5125_CR61","volume-title":"BMC Syst Biol","author":"E Azpeitia","year":"2010","unstructured":"Azpeitia E, Ben\u00edtez M, Vega I, Villarreal C, Alvarez-Buylla ER: Single-cell and coupled GRN models of cell patterning in the Arabidopsis thaliana root stem cell niche. BMC Syst Biol 2010., 4(135):"},{"issue":"5","key":"5125_CR62","doi-asserted-by":"publisher","first-page":"e143","DOI":"10.1371\/journal.pbio.0040143","volume":"4","author":"M Levesque","year":"2006","unstructured":"Levesque M, Vernoux T, Busch W, Cui H, Wang J, Blilou I, Hassan H, Nakajima K, Matsumoto N, Lohmann J, Scheres B, Benfey P: Whole-genome analysis of the SHORT-ROOT developmental pathway in Arabidopsis . PLoS Biol 2006, 4(5):e143. 10.1371\/journal.pbio.0040143","journal-title":"PLoS Biol"},{"issue":"5823","key":"5125_CR63","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1126\/science.1139531","volume":"316","author":"H Cui","year":"2007","unstructured":"Cui H, Levesque M, Vernoux T, Jung J, Paquette A, Gallagher K, Wang J, Blilou I, Scheres B, Benfey P: An evolutionarily conserved mechanism delimiting SHR movement defines a single layer of endodermis in plants. Science 2007, 316(5823):421\u2013425. 10.1126\/science.1139531","journal-title":"Science"},{"issue":"17","key":"5125_CR64","doi-asserted-by":"publisher","first-page":"2196","DOI":"10.1101\/gad.440307","volume":"21","author":"D Welch","year":"2007","unstructured":"Welch D, Hassan H, Blilou I, Immink R, Heidstra R, Scheres B: Arabidopsis JACKDAW and MAGPIE zinc finger proteins delimit asymmetric cell division and stabilize tissue boundaries by restricting SHORT-ROOT action. Genes Dev 2007, 21(17):2196\u20132204. 10.1101\/gad.440307","journal-title":"Genes Dev"},{"issue":"3","key":"5125_CR65","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1101\/gad.252503","volume":"17","author":"S Sabatini","year":"2003","unstructured":"Sabatini S, Heidstra R, Wildwater M, Scheres B: SCARECROW is involved in positioning the stem cell niche in the Arabidopsis root meristem. Genes Dev 2003, 17(3):354\u2013358. 10.1101\/gad.252503","journal-title":"Genes Dev"},{"key":"5125_CR66","volume-title":"Plant Mol Biol","author":"H Ogasawara","year":"2011","unstructured":"Ogasawara H, Kaimi R, Colasanti J, Kozaki A: Activity of transcription factor JACKDAW is essential for SHR\/SCR-dependent activation of SCARECROW and MAGPIE and is modulated by reciprocal interactions with MAGPIE, SCARECROW and SHORT ROOT. Plant Mol Biol 2011, in press."},{"key":"5125_CR67","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1016\/S0092-8674(01)00197-0","volume":"104","author":"H Kaya","year":"2001","unstructured":"Kaya H, Shibahara K, Taoka K, Iwabuchi M, Stillman B, Araki T: FASCIATA genes for chromatin assembly factor-1 in Arabidopsis maintain the cellular organization of apical meristems. Cell 2001, 104: 131\u2013142. 10.1016\/S0092-8674(01)00197-0","journal-title":"Cell"},{"issue":"4","key":"5125_CR68","doi-asserted-by":"publisher","first-page":"879","DOI":"10.1105\/tpc.105.036798","volume":"18","author":"S Inagaki","year":"2006","unstructured":"Inagaki S, Suzuki T, Ohto M, Urawa H, Horiuchi T, Nakamura K, Morikami A: Arabidopsis TEBICHI, with helicase and DNA polymerase domains, is required for regulated cell division and differentiation in meristems. Plant Cell 2006, 18(4):879\u2013892. 10.1105\/tpc.105.036798","journal-title":"Plant Cell"},{"issue":"3","key":"5125_CR69","doi-asserted-by":"publisher","first-page":"336","DOI":"10.1093\/bioinformatics\/btf851","volume":"19","author":"H de Jong","year":"2003","unstructured":"de Jong H, Geiselmann J, Hern\u00e1ndez C, Page M: Genetic Network Analyzer: qualitative simulation of genetic regulatory networks. Bioinformatics 2003, 19(3):336\u2013344. 10.1093\/bioinformatics\/btf851","journal-title":"Bioinformatics"},{"key":"5125_CR70","first-page":"370","volume-title":"IJCAI","author":"G Batt","year":"2005","unstructured":"Batt G, Ropers D, de Jong H, Geiselmann J, Mateescu R, Page M, Schneider D: Analysis and verification of qualitative models of genetic regulatory networks: a model-checking approach. IJCAI 2005, 370\u2013375."},{"key":"5125_CR71","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1016\/j.biosystems.2005.10.005","volume":"84","author":"D Ropers","year":"2006","unstructured":"Ropers D, de Jong H, Page M, Schneider D, Geiselmann J: Qualitative simulation of the carbon starvation response in Escherichia coli. BioSystems 2006, 84: 124\u2013152. 10.1016\/j.biosystems.2005.10.005","journal-title":"BioSystems"},{"key":"5125_CR72","volume-title":"BMC Bioinformatics","author":"PT Monteiro","year":"2009","unstructured":"Monteiro PT, Dumas E, Besson B, Mateescu R, Page M, Freitas AT, de Jong H: A service-oriented architecture for integrating the modeling and formal verification of genetic regulatory networks. BMC Bioinformatics 2009., 10(450): [http:\/\/www.biomedcentral.com\/1471\u20132105\/10\/450]"},{"key":"5125_CR73","doi-asserted-by":"publisher","first-page":"982","DOI":"10.1016\/j.automatica.2007.08.004","volume":"44","author":"G Batt","year":"2008","unstructured":"Batt G, de Jong H, Page M, Geiselmann J: Symbolic reachability analysis of genetic regulatory networks using discrete abstractions. Automatica 2008, 44: 982\u2013989. 10.1016\/j.automatica.2007.08.004","journal-title":"Automatica"},{"key":"5125_CR74","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/978-3-540-88387-6_6","volume-title":"Proc Automated Technology for Verification and Analysis (ATVA)","author":"R Mateescu","year":"2008","unstructured":"Mateescu R, Monteiro PT, Dumas E, de Jong H: Computation Tree Regular Logic for genetic regulatory networks. In Proc Automated Technology for Verification and Analysis (ATVA) Edited by: Cha SS, Choi JY, Kim M, Lee I, Viswanathan M. 2008, 48\u201363. [Lecture Notes in Computer Science No. 5311, Seoul, Korea] [Lecture Notes in Computer Science No. 5311, Seoul, Korea]"},{"issue":"5","key":"5125_CR75","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E Clarke","year":"2003","unstructured":"Clarke E, Grumberg O, Jha S, Lu Y, Veith H: Counterexample-guided abstraction refinement for symbolic model checking. Journal of the ACM 2003, 50(5):752\u2013794. 10.1145\/876638.876643","journal-title":"Journal of the ACM"},{"key":"5125_CR76","volume-title":"Proc 24th Italian Congress on Computational Logic (CILC-09)","author":"A Mosca","year":"2009","unstructured":"Mosca A, Manzoni L, Codecasa D: HyLMoC a model checker for hybrid logic. Proc 24th Italian Congress on Computational Logic (CILC-09) 2009."}],"container-title":["BMC Bioinformatics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1186\/1471-2105-12-490.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,9,1]],"date-time":"2021-09-01T18:43:40Z","timestamp":1630521820000},"score":1,"resource":{"primary":{"URL":"https:\/\/bmcbioinformatics.biomedcentral.com\/articles\/10.1186\/1471-2105-12-490"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,12]]},"references-count":76,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2011,12]]}},"alternative-id":["5125"],"URL":"https:\/\/doi.org\/10.1186\/1471-2105-12-490","relation":{},"ISSN":["1471-2105"],"issn-type":[{"value":"1471-2105","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,12]]},"assertion":[{"value":"31 May 2011","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"22 December 2011","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"22 December 2011","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}],"article-number":"490"}}