Formal Analysis of the Genetic Toggle
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.
KeywordsModel Check Theorem Prove Operational Semantic Genetic Network Network Motif
Unable to display preview. Download preview PDF.
- 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
- 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
- 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