Formal Analysis of the Genetic Toggle

  • Giampaolo Bella
  • Pietro Liò
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5688)


The formal analysis of the toggle switch, which is among the most common motifs of genetic networks, shows that along with the powerful development of mathematical modelling, formal methods can be of great help in investigating the properties of genetic networks. In particular, a general approach to modelling genetic networks through the language of higher-order logic is advanced and mechanised in the theorem prover Isabelle. An inductive definition provides a formal model for the genetic toggle as the set of all possible evolutions of such network. Gene polymerase and protein concentration are formalised as primitive recursive functions. The main properties of the genetic toggle are confirmed upon the model: it is possible that one protein exceeds a stated concentration threshold and the other protein does not; it is impossible that both proteins exceed their respective concentration thresholds at the same time. To the best of the authors’ knowledge, this is the first contribution of theorem proving in the area of genetic network analysis, and as such may set the foundations for a new niche of research.


Model Check Theorem Prove Operational Semantic Genetic Network Network Motif 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Yeger-Lotem, E., et al.: Network motifs in integrated cellular networks of transcription-regulation and protein-protein interaction. Proc. Natl. Acad. Sci. U.S.A. 101, 5934–5939 (2004)CrossRefPubMedPubMedCentralGoogle Scholar
  2. 2.
    Tyson, J.J., Chen, K.C., Novak, B.: Sniffers, buzzers, toggles and blinkers: dynamics of regulatory and signaling pathways in the cell. Curr. Opin. Cell Biol. 15, 221–231 (2003)CrossRefPubMedGoogle Scholar
  3. 3.
    Ninfa, A.J., Selinsky, S., Perry, N., Atkins, S., Xiu Song, Q., Mayo, A., Arps, D., Woolf, P., Atkinson, M.R.: Using two-component systems and other bacterial regulatory factors for the fabrication of synthetic genetic devices. Meth. Enzymol. 422, 488–512 (2007)CrossRefPubMedPubMedCentralGoogle Scholar
  4. 4.
    Atkinson, M.R., Savageau, M.A., Myers, J.T., Ninfa, A.J.: Development of genetic circuitry exhibiting toggle switch or oscillatory behavior in Escherichia coli. Cell 113, 597–607 (2003)CrossRefPubMedGoogle Scholar
  5. 5.
    Gillespie, D.: Exact simulation of coupled chemical reactions. Journal of Chemical Physics 81, 2340–2345 (1997)CrossRefGoogle Scholar
  6. 6.
    Batt, G., de Jong, H., Geiselmann, J., Page, M.: Analysis of genetic regulatory networks: a model-checking approach. In: Benerecetti, M., Pecheur, C. (eds.) Working Notes of the Second Workshop on Model Checking and Artificial Intelligence, MoChArt 2003, Acapulco, Mexico, pp. 51–58 (2003)Google Scholar
  7. 7.
    Batt, G., Bergamini, D., de Jong, H., Garavel, H., Mateescu, R.: Model checking genetic regulatory networks using GNA and CADP. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 158–163. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  8. 8.
    McMillan, K.: Symbolic Model Checking. Kluwer Academic Publisher, Dordrecht (1993)CrossRefGoogle Scholar
  9. 9.
    Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)Google Scholar
  10. 10.
    Bella, G.: Formal Correctness of Security Protocols. Information Security and Cryptography. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  11. 11.
    Gardner, T.S., Cantor, C.R., Collins, J.J.: Construction of a genetic toggle switch in Escherichia coli. Nature 403, 339–342 (2000)CrossRefPubMedGoogle Scholar
  12. 12.
    Tian, T., Xu, S., Gao, J., Burrage, K.: Simulated maximum likelihood method for estimating kinetic rates in gene expression. Bioinformatics 23, 84–91 (2007)CrossRefPubMedGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Giampaolo Bella
    • 1
  • Pietro Liò
    • 2
  1. 1.Dipartimento di Matematica e InformaticaUniversità di CataniaCataniaItaly
  2. 2.Computer LaboratoryUniversity of CambridgeCambridgeUK

Personalised recommendations