Synthetic biology is an interdisciplinary field that uses well-established engineering principles for performing the analysis of the biological systems, such as biological circuits, pathways, controllers and enzymes. Conventionally, the analysis of these biological systems is performed using paper-and-pencil proofs and computer simulation methods. However, these methods cannot ensure accurate results due to their inherent limitations. Higher-order-logic (HOL) theorem proving is proposed and used as a complementary approach for analysing linear biological systems, which is based on developing a mathematical model of the genetic circuits and the bio-controllers used in synthetic biology based on HOL and analysing it using deductive reasoning in an interactive theorem prover. The involvement of the logic, mathematics and the deductive reasoning in this method ensures the accuracy of the analysis. It is proposed to model the continuous dynamics of the genetic circuits and their associated controllers using differential equations and perform their transfer function-based analysis using the Laplace transform in a theorem prover. For illustration, the genetic circuits of activated and repressed expressions and autoactivation of protein, and phase lag and lead controllers, which are widely used in cancer-cell identifiers and multi-input receptors for precise disease detection, are formally analyzed.

References

1. 1)
  - 7. Benner, S.A., Sismour, A.M.: ‘Synthetic biology’, Nat. Rev. Genetics, 2005, 6, (7), p. 533.
2. 2)
  - 42. Walter, C.: ‘Stability of controlled biological systems’, J. Theor. Biol., 1969, 23, (1), pp. 23–38.
3. 3)
  - 24. Ahmad, S., Hasan, O., Siddique, U., et al: ‘Formalization of zsyntax to reason about molecular pathways in HOL4’. Brazilian Symp. on Formal Methods, Belo Horizonte, Brazil, 2014, pp. 32–47.
4. 4)
  - 34. Chen, Y.J., Dalchau, N., Srinivas, N., et al: ‘Programmable chemical controllers made from DNA’, Nat. Nanotechnol., 2013, 8, (10), p. 755.
5. 5)
  - 16. Camilleri, A., Gordon, M., Melham, T.: ‘Hardware verification using higher-order logic’, University of Cambridge, Computer Laboratory, 1986.
6. 6)
  - 4. Baldwin, G.: ‘Synthetic biology’ (John Wiley & Sons, New Jersey, USA, 2012).
7. 7)
  - 9. Nise, N.S.: ‘Control systems engineering’ (John Wiley & Sons, New Jersey, USA, 2007).
8. 8)
  - 6. Andrianantoandro, E., Basu, S., Karig, D.K., et al: ‘Synthetic biology: new engineering rules for an emerging discipline’, Mol. Syst. Biol., 2006, 2, (1), pp. 1–14, Article number 2006.0028.
9. 9)
  - 37. Gardner, T.S., Cantor, C.R., Collins, J.J.: ‘Construction of a genetic toggle switch in Escherichia coli’, Nature, 2000, 403, (6767), p. 339.
10. 10)
  - 2. Alon, U.: ‘An Introduction to systems biology: design principles of biological circuits’ (Chapman and Hall/CRC, New York, USA, 2006).
11. 11)
  - 29. Abrams, M.: ‘A history of OCaml’, 2015, . Available at http://ocaml.org/learn/history.html.
12. 12)
  - 17. Schumann, J.M.: ‘Automated theorem proving in software engineering’ (Springer Science & Business Media, Berlin Heidelberg, Germany, 2001).
13. 13)
  - 10. De Zeeuw, R.A., Baker, G.B., Coutts, R.T., et al: ‘Evaluation of analytical methods in biological systems: analysis of biogenic amines’, vol. 4 (Elsevier, Amsterdam, Netherlands, 1982).
14. 14)
  - 41. Shin, Y.J., Bleris, L.: ‘Linear control theory for gene network modeling’, PloS One, 2010, 5, (9), p. e12785.
15. 15)
  - 15. Rashid, A., Hasan, O., Siddique, U., et al: ‘Formal reasoning about systems biology using theorem proving’, PLOS ONE, 2017, 12, (7), p. e0180179.
16. 16)
  - 11. Haefner, J.W.: ‘Modeling biological systems: principles and applications’ (Springer Science & Business Media, New York, USA, 2005).
17. 17)
  - 38. Abed, S., Rashid, A., Hasan, O.: ‘Formal reasoning about synthetic biology using higher-order-logic theorem proving’, 2020, Available at http://save.seecs.nust.edu.pk/frsbholtp/.
18. 18)
  - 21. Bartocci, E., Bortolussi, L., Nenzi, L.: ‘A temporal logic approach to modular design of synthetic biological circuits’. Computational Methods in Systems Biology, Klosterneuburg, Austria, 2013, pp. 164–177.
19. 19)
  - 30. Taqdees, S.H., Hasan, O.: ‘Formalization of Laplace transform using the multivariable Calculus theory of HOL-light’. Logic for Programming, Artificial Intelligence, and Reasoning, Stellenbosch, South Africa, 2013 (LNCS, 8312), pp. 744–758.
20. 20)
  - 20. Yordanov, B., Appleton, E., Ganguly, R., et al: ‘Experimentally driven verification of synthetic biological circuits’. Design, Automation & Test in Europe, Dresden, Germany, 2012, pp. 236–241.
21. 21)
  - 12. Gaylord, R.J., Wellin, P.R., Titus, B., et al: ‘Computer simulations with Mathematica: explorations in complex physical and biological systems’, Comput. Phys., 1996, 10, (4), pp. 349–350.
22. 22)
  - 36. Rosenfeld, N., Elowitz, M.B., Alon, U.: ‘Negative autoregulation speeds the response times of transcription networks’, J. Mol. Biol., 2002, 323, (5), pp. 785–793.
23. 23)
  - 31. Rashid, A., Hasan, O.: ‘Formalization of transform methods using HOL light’. Conf. on Intelligent Computer Mathematics, Edinburgh, Scotland, 2017 (LNAI, 10383), pp. 319–332.
24. 24)
  - 5. Ogata, K., Yang, Y.: ‘Modern control engineering’, vol. 4 (London, London, UK, 2002).
25. 25)
  - 23. Clarke, E.M., Grumberg, O., Jha, S., et al: ‘Progress on the state explosion problem in model checking’, in Wilhelm, R., et al (Eds.): ‘informatics’ (Springer, Berlin Heidelberg, Germany, 2001), pp. 176–194.
26. 26)
  - 40. Houpis, C.H., Sheldon, S.N.: ‘Linear control system analysis and design with MATLAB’ (CRC Press, Florida, USA, 2013).
27. 27)
  - 26. Abed, S., Rashid, A., Hasan, O.: ‘Formal analysis of the biological circuits using higher-order-logic theorem proving’. Symp. on Applied Computing, SAC ’20 ACM, New York, NY, USA, 2020, pp. 3–7.
28. 28)
  - 3. Alberts, B.: ‘Molecular biology of the cell’ (Garland Science, New York, USA, 2017).
29. 29)
  - 19. Hasan, O., Tahar, S.: ‘Formal verification methods’, in Mehdi, Khosrow-Pour, et al (Eds.): ‘Encyclopedia of information science and technology’ (IGI Global, Pennsylvania, United States, 2015, 3rd edn.), pp. 7162–7170.
30. 30)
  - 1. Muschler, G.F., Nakamoto, C., Griffith, L.G.: ‘Engineering principles of clinical cell-based tissue engineering’, J. Bone Joint Surg., 2004, 86, (7), pp. 1541–1558.
31. 31)
  - 27. Harrison, J.: ‘Handbook of practical logic and automated reasoning’ (Cambridge University Press, Cambridge, UK, 2009).
32. 32)
  - 33. Azimi, S., Iancu, B., Petre, I.: ‘Reaction system models for the heat shock response’, Fundam. Inform., 2014, 131, (3), pp. 299–312.
33. 33)
  - 35. Yordanov, B., Kim, J., Petersen, R.L., et al: ‘Computational design of nucleic acid feedback control circuits’, ACS Synth. Biol., 2014, 3, (8), pp. 600–616.
34. 34)
  - 13. Harrison, J., Théry, L.: ‘Extending the HOL theorem prover with a computer algebra system to reason about the reals’. HOL Users’ Group Workshop, Vancouver, B. C., Canada, 1993, pp. 174–184.
35. 35)
  - 32. Pilling, M.J., Seakins, P.W.: ‘Reaction kinetics’ (Oxford University Press, Oxford, UK, 1996).
36. 36)
  - 25. Ahmad, S., Hasan, O., Siddique, U.: ‘On the formalization of zsyntax with applications in molecular biology’, Scalable Comput.: Pract. Exp., 2015, 16, (1), pp. 37–52.
37. 37)
  - 14. Clarke, E.M., Wing, J.M.: ‘Formal methods: state of the art and future directions’, ACM Comput. Surv., 1996, 28, (4), pp. 626–643.
38. 38)
  - 39. Ingalls, B.P.: ‘Mathematical modeling in systems biology: an Introduction’ (MIT Press, Massachusetts, USA, 2013).
39. 39)
  - 18. Grumberg, O., Clarke, E.M., Peled, D.: ‘Model checking’ (The MIT Press Cambridge, Cambridge, UK, 1999).
40. 40)
  - 28. Harrison, J.: ‘HOL light: a tutorial introduction’. Formal Methods in Computer-Aided Design, Palo Alto, CA, USA, 1996 (LNCS, 1166), pp. 265–269.
41. 41)
  - 8. Harris, A.W., Dolan, J.A., Kelly, C.L., et al: ‘Designing genetic feedback controllers’, IEEE Trans. Biomed. Circuits Syst., 2015, 9, (4), pp. 475–484.
42. 42)
  - 22. Madsen, C., Myers, C.J., Roehner, N., et al: ‘Utilizing stochastic model checking to analyze genetic circuits’. IEEE Symp. on Computational Intelligence in Bioinformatics and Computational Biology, San Diego, California, USA, 2012, pp. 379–386.

Formal reasoning about synthetic biology using higher-order-logic theorem proving

References

Related content