{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,14]],"date-time":"2026-02-14T08:32:33Z","timestamp":1771057953143,"version":"3.50.1"},"reference-count":49,"publisher":"Springer Science and Business Media LLC","issue":"1","content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["BMC Syst Biol"],"published-print":{"date-parts":[[2007,12]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:sec>\n            <jats:title>Background<\/jats:title>\n            <jats:p>A central goal of Systems Biology is to model and analyze biological signaling pathways that interact with one another to form complex networks. Here we introduce <jats:italic>Qualitative networks<\/jats:italic>, an extension of <jats:italic>Boolean networks<\/jats:italic>. With this framework, we use formal verification methods to check whether a model is consistent with the laboratory experimental observations on which it is based. If the model does not conform to the data, we suggest a revised model and the new hypotheses are tested in-silico.<\/jats:p>\n          <\/jats:sec>\n          <jats:sec>\n            <jats:title>Results<\/jats:title>\n            <jats:p>We consider networks in which elements range over a small finite domain allowing more flexibility than Boolean values, and add target functions that allow to model a rich set of behaviors. We propose a symbolic algorithm for analyzing the steady state of these networks, allowing us to scale up to a system consisting of 144 elements and state spaces of approximately 10<jats:sup>86<\/jats:sup> states. We illustrate the usefulness of this approach through a model of the interaction between the Notch and the Wnt signaling pathways in mammalian skin, and its extensive analysis.<\/jats:p>\n          <\/jats:sec>\n          <jats:sec>\n            <jats:title>Conclusion<\/jats:title>\n            <jats:p>We introduce an approach for constructing computational models of biological systems that extends the framework of Boolean networks and uses formal verification methods for the analysis of the model. This approach can scale to multicellular models of complex pathways, and is therefore a useful tool for the analysis of complex biological systems. The hypotheses formulated during in-silico testing suggest new avenues to explore experimentally. Hence, this approach has the potential to efficiently complement experimental studies in biology.<\/jats:p>\n          <\/jats:sec>","DOI":"10.1186\/1752-0509-1-4","type":"journal-article","created":{"date-parts":[[2007,1,9]],"date-time":"2007-01-09T07:21:25Z","timestamp":1168327285000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":68,"title":["Qualitative networks: a symbolic approach to analyze biological signaling networks"],"prefix":"10.1186","volume":"1","author":[{"given":"Marc A","family":"Schaub","sequence":"first","affiliation":[]},{"given":"Thomas A","family":"Henzinger","sequence":"additional","affiliation":[]},{"given":"Jasmin","family":"Fisher","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2007,1,8]]},"reference":[{"key":"4_CR1","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1146\/annurev.genom.2.1.343","volume":"2","author":"T Ideker","year":"2001","unstructured":"Ideker T, Galitski T, Hood L: A new approach to decoding life: systems biology. Annu Rev Genomics Hum Genet. 2001, 2: 343-372.","journal-title":"Annu Rev Genomics Hum Genet"},{"issue":"5560","key":"4_CR2","doi-asserted-by":"publisher","first-page":"1662","DOI":"10.1126\/science.1069492","volume":"295","author":"H Kitano","year":"2002","unstructured":"Kitano H: Systems biology: a brief overview. Science. 2002, 295 (5560): 1662-1664.","journal-title":"Science"},{"issue":"3737","key":"4_CR3","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1007\/11599128_10","volume":"III","author":"L Cardelli","year":"2005","unstructured":"Cardelli L: Abstract Machines of Systems Biology. Transactions on Computational Systems Biology. 2005, III (3737): 145-168.","journal-title":"Transactions on Computational Systems Biology"},{"issue":"11","key":"4_CR4","doi-asserted-by":"publisher","first-page":"2485","DOI":"10.1101\/gr.1215303","volume":"13","author":"S Efroni","year":"2003","unstructured":"Efroni S, Harel D, Cohen IR: Toward rigorous comprehension of biological complexity: modeling, execution, and visualization of thymic T-cell maturation. Genome Res. 2003, 13 (11): 2485-2497.","journal-title":"Genome Res"},{"key":"4_CR5","first-page":"4","volume-title":"CMSB","author":"N Kam","year":"2003","unstructured":"Kam N, Harel D, Kugler H, Marelly R, Pnueli A, Hubbard EJA, Stern MJ: Formal Modeling of C. elegans Development: A Scenario-Based Approach. CMSB. 2003, 4-20."},{"issue":"6","key":"4_CR6","doi-asserted-by":"publisher","first-page":"1951","DOI":"10.1073\/pnas.0409433102","volume":"102","author":"J Fisher","year":"2005","unstructured":"Fisher J, Piterman N, Hubbard EJ, Stern MJ, Harel D: Computational insights into Caenorhabditis elegans vulval development. Proc Natl Acad Sci USA. 2005, 102 (6): 1951-1956.","journal-title":"Proc Natl Acad Sci USA"},{"issue":"12","key":"4_CR7","doi-asserted-by":"publisher","first-page":"6750","DOI":"10.1073\/pnas.95.12.6750","volume":"95","author":"PJ Goss","year":"1998","unstructured":"Goss PJ, Peccoud J: Quantitative modeling of stochastic systems in molecular biology by using stochastic Petri nets. Proc Natl Acad Sci USA. 1998, 95 (12): 6750-6755.","journal-title":"Proc Natl Acad Sci USA"},{"issue":"2","key":"4_CR8","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1197\/jamia.M1637","volume":"12","author":"M Peleg","year":"2005","unstructured":"Peleg M, Rubin D, Altman RB: Using Petri Net tools to study properties and dynamics of biological systems. J Am Med Inform Assoc. 2005, 12 (2): 181-199.","journal-title":"J Am Med Inform Assoc"},{"key":"4_CR9","volume-title":"Proceedings of the First Annual Recomb Satellite Workshop on Systems Biology","author":"DL Dill","year":"2005","unstructured":"Dill DL, Knapp MA, Gage P, Talcott C, Laderoute K, Lincoln P: The Pathalyzer: a Tool for Analysis of Signal Transduction Pathways. Proceedings of the First Annual Recomb Satellite Workshop on Systems Biology. 2005"},{"key":"4_CR10","first-page":"19","volume-title":"HSCC","author":"R Alur","year":"2001","unstructured":"Alur R, Belta C, Ivancic F: Hybrid Modeling and Simulation of Biomolecular Networks. HSCC. 2001, 19-32."},{"key":"4_CR11","first-page":"233","volume-title":"Hybrid Systems: Computation and Control HSCC, Volume 2623 of LNCS. Springer","author":"R Ghosh","year":"2003","unstructured":"Ghosh R, Tiwari A, Tomlin C: Automated Symbolic Reachability Analysis with Application to Delta-Notch Signaling Automata. Hybrid Systems: Computation and Control HSCC, Volume 2623 of LNCS. Springer. Edited by: Maler O, Pnueli A. 2003, 233-248."},{"key":"4_CR12","doi-asserted-by":"publisher","first-page":"1675","DOI":"10.1109\/WSC.2006.322942","volume-title":"Executable Biology. Proc. of the 2006 Winter Simulation Conference \u2013 Track on Modeling and Simulation in Computational Biology","author":"J Fisher","year":"2006","unstructured":"Fisher J, Henzinger TA: Executable Biology. Executable Biology. Proc. of the 2006 Winter Simulation Conference \u2013 Track on Modeling and Simulation in Computational Biology. 2006, 1675-1682."},{"key":"4_CR13","volume-title":"Model Checking","author":"E Clarke","year":"2000","unstructured":"Clarke E, Grumberg O, Peled D: Model Checking. 2000, Cambridge, MA: MIT Press"},{"key":"4_CR14","first-page":"236","volume-title":"CMSB","author":"J Fisher","year":"2004","unstructured":"Fisher J, Harel D, Hubbard EJA, Piterman N, Stern MJ, Swerdlin N: Combining State-Based and Scenario-Based Approaches in Modeling Biological Systems. CMSB. 2004, 236-241."},{"key":"4_CR15","first-page":"149","volume-title":"CMSB","author":"N Chabrier","year":"2003","unstructured":"Chabrier N, Fages F: Symbolic Model Checking of Biochemical Networks. CMSB. 2003, 149-162."},{"issue":"3","key":"4_CR16","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. J Theor Biol. 2004, 229 (3): 339-347.","journal-title":"J Theor Biol"},{"issue":"Suppl 1","key":"4_CR17","doi-asserted-by":"publisher","first-page":"19","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): 19-19.","journal-title":"Bioinformatics"},{"issue":"1\u20133","key":"4_CR18","first-page":"13","volume":"67","author":"R Barbuti","year":"2005","unstructured":"Barbuti R, Cataudella S, Maggiolo-Schettini A, Milazzo P, Troina A: A Probabilistic Model for Molecular Systems. Fundamenta Informaticae. 2005, 67 (1\u20133): 13-27.","journal-title":"Fundamenta Informaticae"},{"key":"4_CR19","first-page":"32","volume-title":"CMSB","author":"J Heath","year":"2006","unstructured":"Heath J, Kwiatkowska M, Norman G, Parker D, Tymchyshyn O: Probabilistic model checking of complex biological pathways. CMSB. 2006, 32-48."},{"issue":"3","key":"4_CR20","doi-asserted-by":"publisher","first-page":"437","DOI":"10.1016\/0022-5193(69)90015-0","volume":"22","author":"SA Kauffman","year":"1969","unstructured":"Kauffman SA: Metabolic stability and epigenesis in randomly constructed genetic nets. Journal of Theoretical Biology. 1969, 22 (3): 437-467.","journal-title":"Journal of Theoretical Biology"},{"issue":"3","key":"4_CR21","doi-asserted-by":"publisher","first-page":"563","DOI":"10.1016\/0022-5193(73)90247-6","volume":"42","author":"R Thomas","year":"1973","unstructured":"Thomas R: Boolean formalization of genetic control circuits. J Theor Biol. 1973, 42 (3): 563-585.","journal-title":"J Theor Biol"},{"issue":"2","key":"4_CR22","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1006\/jtbi.1998.0701","volume":"193","author":"L Mendoza","year":"1998","unstructured":"Mendoza L, Alvarez-Buylla ER: Dynamics of the genetic regulatory network for Arabidopsis thaliana flower morphogenesis. J Theor Biol. 1998, 193 (2): 307-319.","journal-title":"J Theor Biol"},{"key":"4_CR23","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1006\/excr.2000.5044","volume":"261","author":"S Huang","year":"2000","unstructured":"Huang S, Ingber DE: Shape-dependent control of cell growth, differentiation, and apoptosis: switching between attractors in cell regulatory networks. Exp Cell Res. 2000, 261: 91-103.","journal-title":"Exp Cell Res"},{"key":"4_CR24","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-18.","journal-title":"J Theor Biol"},{"issue":"14","key":"4_CR25","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-4786.","journal-title":"Proc Natl Acad Sci USA"},{"issue":"2","key":"4_CR26","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1093\/bioinformatics\/18.2.261","volume":"18","author":"I Shmulevich","year":"2002","unstructured":"Shmulevich I, Dougherty ER, Kim S, Zhang W: Probabilistic Boolean Networks: a rule-based uncertainty model for gene regulatory networks. Bioinformatics. 2002, 18 (2): 261-274.","journal-title":"Bioinformatics"},{"issue":"2","key":"4_CR27","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 \u2013 I. Biological role of feedback loops and practical use of the concept of the loop-characteristic state. Bull Math Biol. 1995, 57 (2): 247-276.","journal-title":"Bull Math Biol"},{"issue":"6","key":"4_CR28","doi-asserted-by":"publisher","first-page":"1025","DOI":"10.1016\/S0092-8240(03)00061-2","volume":"65","author":"V Devloo","year":"2003","unstructured":"Devloo V, Hansen P, Labb\u00e9 M: Identification of all steady states in large networks by logical analysis. Bull Math Biol. 2003, 65 (6): 1025-1051.","journal-title":"Bull Math Biol"},{"issue":"8","key":"4_CR29","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"RE Bryant","year":"1986","unstructured":"Bryant RE: Graph-Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers. 1986, 35 (8): 677-691.","journal-title":"IEEE Transactions on Computers"},{"key":"4_CR30","first-page":"403","volume-title":"DAC","author":"JR Burch","year":"1991","unstructured":"Burch JR, Clarke EM, Long DE: Representing Circuits More Efficiently in Symbolic Model Checking. DAC. 1991, 403-407."},{"issue":"5594","key":"4_CR31","doi-asserted-by":"publisher","first-page":"824","DOI":"10.1126\/science.298.5594.824","volume":"298","author":"R Milo","year":"2002","unstructured":"Milo R, Shen-Orr S, Itzkovitz S, Kashtan N, Chklovskii D, Alon U: Network motifs: Simple building blocks of complex networks. Science. 2002, 298 (5594): 824-828.","journal-title":"Science"},{"issue":"21","key":"4_CR32","doi-asserted-by":"publisher","first-page":"11980","DOI":"10.1073\/pnas.2133841100","volume":"100","author":"S Mangan","year":"2003","unstructured":"Mangan S, Alon U: Structure and function of the feed-forward loop network motif. Proc Natl Acad Sci USA. 2003, 100 (21): 11980-11985.","journal-title":"Proc Natl Acad Sci USA"},{"issue":"5","key":"4_CR33","doi-asserted-by":"publisher","first-page":"1073","DOI":"10.1016\/j.jmb.2005.12.003","volume":"356","author":"S Mangan","year":"2006","unstructured":"Mangan S, Itzkovitz S, Zaslaver A, Alon U: The incoherent feed-forward loop accelerates the response-time of the gal system of Escherichia coli. J Mol Biol. 2006, 356 (5): 1073-1081.","journal-title":"J Mol Biol"},{"issue":"12","key":"4_CR34","doi-asserted-by":"publisher","first-page":"1118","DOI":"10.1002\/bies.10189","volume":"24","author":"H Bolouri","year":"2002","unstructured":"Bolouri H, Davidson EH: Modeling transcriptional regulatory networks. Bioessays. 2002, 24 (12): 1118-1129.","journal-title":"Bioessays"},{"issue":"10","key":"4_CR35","doi-asserted-by":"publisher","first-page":"756","DOI":"10.1038\/nrc1186","volume":"3","author":"F Radtke","year":"2003","unstructured":"Radtke F, Raj K: The role of Notch in tumorigenesis: oncogene or tumour suppressor?. Nat Rev Cancer. 2003, 3 (10): 756-767.","journal-title":"Nat Rev Cancer"},{"issue":"7035","key":"4_CR36","doi-asserted-by":"publisher","first-page":"843","DOI":"10.1038\/nature03319","volume":"434","author":"T Reya","year":"2005","unstructured":"Reya T, Clevers H: signalling in stem cells and cancer. Nature. 2005, 434 (7035): 843-850.","journal-title":"Nature"},{"key":"4_CR37","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1146\/annurev.cellbio.14.1.59","volume":"14","author":"A Wodarz","year":"1998","unstructured":"Wodarz A, Nusse R: Mechanisms of Wnt signaling in development. Annu Rev Cell Dev Biol. 1998, 14: 59-88.","journal-title":"Annu Rev Cell Dev Biol"},{"key":"4_CR38","doi-asserted-by":"publisher","first-page":"6057","DOI":"10.1128\/MCB.17.10.6057","volume":"17","author":"B Luo","year":"1997","unstructured":"Luo B, Aster JC, Hasserjian RP, Kuo F, Sklar J: Isolation and Functional Analysis of a cDNA for Human Jagged2, a gene Encoding a Ligand for the Notchl Receptor. Mol Cell Biol. 1997, 17: 6057-6067.","journal-title":"Mol Cell Biol"},{"key":"4_CR39","doi-asserted-by":"publisher","first-page":"3427","DOI":"10.1093\/emboj\/20.13.3427","volume":"20","author":"A Rangarajan","year":"2001","unstructured":"Rangarajan A, Talora C, Okuyama R, Nicolas M, Mammucari C, Oh H, Aster JC, Krishna S, Metzger D, Chambon P, Miele L, Aguet M, Radtke F, Dotto GP: Notch Signaling is a Direct Determinant of Keratinocyte Growth Arrest and Entry into Differentiation. EMBO J. 2001, 20: 3427-3436.","journal-title":"EMBO J"},{"issue":"3","key":"4_CR40","doi-asserted-by":"publisher","first-page":"416","DOI":"10.1038\/ng1099","volume":"33","author":"M Nicolas","year":"2003","unstructured":"Nicolas M, Wolfer A, Raj K, Kummer J, Mill P, van Noort M, Hui C, Clevers H, Dotto G, Radtke F: Notchl functions as a tumor suppressor in mouse skin. Nat Genet. 2003, 33 (3): 416-421.","journal-title":"Nat Genet"},{"key":"4_CR41","doi-asserted-by":"publisher","first-page":"1485","DOI":"10.1101\/gad.341405","volume":"19","author":"V Devgan","year":"2005","unstructured":"Devgan V, Mammucari C, Millar SE, Brisken C, Dotto GP: p21WAFl\/Cipl is a Negative Transcriptional Regulator of Wnt4 Expression Downstream of Notchl Activation. Genes Dev. 2005, 19: 1485-1495.","journal-title":"Genes Dev"},{"issue":"9","key":"4_CR42","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1016\/S0960-9822(00)00451-6","volume":"10","author":"S Lowell","year":"2000","unstructured":"Lowell S, Jones P, Le Roux I, Dunne J, Watt F: Stimulation of human epidermal differentiation by delta-notch signalling at the boundaries of stem-cell clusters. Curr Biol. 2000, 10 (9): 491-500.","journal-title":"Curr Biol"},{"issue":"5","key":"4_CR43","doi-asserted-by":"publisher","first-page":"785","DOI":"10.1016\/S0022-2836(02)00994-4","volume":"323","author":"N Rosenfeld","year":"2002","unstructured":"Rosenfeld N, Elowitz MB, Alon U: Negative autoregulation speeds the response times of transcription networks. J Mol Biol. 2002, 323 (5): 785-793.","journal-title":"J Mol Biol"},{"key":"4_CR44","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1007\/BFb0028765","volume-title":"CAV 98: Computer-Aided Verification","author":"T Henzinger","year":"1998","unstructured":"Henzinger T, Qadeer S, Rajamani S: You assume, we guarantee: Methodology and case studies. CAV 98: Computer-Aided Verification. 1998, 440-451. Lecture Notes in Computer Science 1427, Springer"},{"key":"4_CR45","first-page":"154","volume-title":"CAV","author":"EM Clarke","year":"2000","unstructured":"Clarke EM, Grumberg O, Jha S, Lu Y, Veith H: Counterexample-Guided Abstraction Refinement. CAV. 2000, 154-169."},{"key":"4_CR46","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1008739929481","volume":"15","author":"R Alur","year":"1999","unstructured":"Alur R, Henzinger T: Reactive modules. Formal Methods in System Design. 1999, 15: 7-48.","journal-title":"Formal Methods in System Design"},{"key":"4_CR47","first-page":"835","volume-title":"Proceedings of the 23rd Annual International Conference on Software Engineering","author":"R Alur","year":"2001","unstructured":"Alur R, de Alfaro L, Grosu R, Henzinger T, Kang M, Kirsch C, Majumdar R, Mang F, Wang B: JMocHA: A model-checking tool that exploits design structure. Proceedings of the 23rd Annual International Conference on Software Engineering. 2001, 835-836. IEEE Computer Society Press"},{"issue":"2","key":"4_CR48","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"JR Burch","year":"1992","unstructured":"Burch JR, Clarke EM, McMillan KL, Dill DL, Hwang LJ: Symbolic Model Checking: 1020 States and Beyond. Inf Comput. 1992, 98 (2): 142-170.","journal-title":"Inf Comput"},{"key":"4_CR49","first-page":"807","volume-title":"Proceedings of the 28th International Conference on Software Engineering (ICSE 2006, Shanghai, May 20\u201328)","author":"D Beyer","year":"2006","unstructured":"Beyer D: Relational Programming with CrocoPat. Proceedings of the 28th International Conference on Software Engineering (ICSE 2006, Shanghai, May 20\u201328). 2006, 807-810. ACM Press, http:\/\/www.cs.sfu.ca\/~dbeyer\/CrocoPat\/"}],"container-title":["BMC Systems Biology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1186\/1752-0509-1-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,9,1]],"date-time":"2021-09-01T03:08:06Z","timestamp":1630465686000},"score":1,"resource":{"primary":{"URL":"https:\/\/bmcsystbiol.biomedcentral.com\/articles\/10.1186\/1752-0509-1-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,1,8]]},"references-count":49,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2007,12]]}},"alternative-id":["4"],"URL":"https:\/\/doi.org\/10.1186\/1752-0509-1-4","relation":{},"ISSN":["1752-0509"],"issn-type":[{"value":"1752-0509","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,1,8]]},"assertion":[{"value":"10 August 2006","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 January 2007","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 January 2007","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}],"article-number":"4"}}