Automated Reasoning for the Synthesis and Analysis of Biological Programs

  • Sara-Jane DunnEmail author
  • Boyan Yordanov
Part of the Computational Biology book series (COBO, volume 30)


Cellular decision-making arises as the output of biochemical information processing, as complex cascades of molecular interactions are triggered by input stimuli. Deciphering critical interactions and how they are organised into biological programs is a huge challenge, compounded by the difficulty of manually navigating alternative hypotheses consistent with observed behaviour. Against this backdrop, automated reasoning is a powerful methodology to tackle biological complexity and derive explanations of behaviour that are provably consistent with experimental evidence. We present a reasoning framework that permits the synthesis and analysis of a set of dynamic biological interaction networks. Employing methods based on Satisfiability Modulo Theories (SMT), we encode experimental observations as specifications of expected dynamics, and synthesise networks consistent with these constraints. Predictions of untested behaviour are generated based on all consistent models, without requiring time-consuming simulation or state space exploration, and the method can be used to identify additional components, topological ‘switches’ that allow cell state changes, and to predict gene-level dynamics. We show the reader how to utilise this reasoning framework to encode and explore rich queries for their biological system of choice.


  1. 1.
    Abou-Jaoudé W, Monteiro PT, Naldi A, Grandclaudon M, Soumelis V, Chaouiya C et al (2015) Model checking to assess T-helper cell plasticity. Front Bioeng Biotechnol 2Google Scholar
  2. 2.
    Bartocci E, Lió P (2016) Computational modeling, formal analysis, and tools for systems biology. PLoS Comput Biol 12(1):1–22CrossRefGoogle Scholar
  3. 3.
    Benque D, Bourton S, Cockerton C, Cook B, Fisher J, Ishtiaq S et al (2012) BMA: visual tool for modeling and analyzing biological networks. Lecture notes in computer science (including subseries Lecture notes in artificial intelligence and Lecture notes in bioinformatics). LNCS, vol 7358, pp 686–692CrossRefGoogle Scholar
  4. 4.
    Biere A, Cimatti A, Clarke E, Zhu Y (1999) Symbolic model checking without BDDs. In: Cleaveland WR (ed) Tools and algorithms for the construction and analysis of systems. Lecture notes in computer science, vol 1579. Springer, Berlin, pp 193–207CrossRefGoogle Scholar
  5. 5.
    Bjorner N, Moura LD (2011) Satisfiability modulo theories: introduction and applications. Commun ACM 54(9):69–77CrossRefGoogle Scholar
  6. 6.
    Chabrier N, Fages F (2003) Symbolic model checking of biochemical networks. Lect Notes Comput Sci 2602:149–162Google Scholar
  7. 7.
    Corblin F, Fanchon E, Trilling L (2010) Applications of a formal approach to decipher discrete genetic networks. BMC Bioinform 11:385CrossRefGoogle Scholar
  8. 8.
    Corblin F, Tripodi S, Fanchon E, Ropers D, Trilling L (2009) A declarative constraint-based method for analyzing discrete genetic regulatory networks. Biosystems 98(2):91–104CrossRefGoogle Scholar
  9. 9.
    De Moura L, Bjørner N (2008) Z3: an efficient SMT solver. Tools and algorithms for the construction and analysis of systems. Springer, Berlin, pp 337–340Google Scholar
  10. 10.
    Dunn SJ, Li MA, Carbognin E, Smith AG, Martello G (2018) A common molecular logic determines embryonic stem cell self-renewal and reprogramming. bioRxiv, p 200501Google Scholar
  11. 11.
    Dunn SJ, Martello G, Yordanov B, Emmott S, Smith AG (2014) Defining an essential transcription factor program for naive pluripotency. Science 344(6188):1156–1160CrossRefGoogle Scholar
  12. 12.
    Fages F (2002) Modelling and querying interaction networks in the biochemical abstract machine BIOCHAM. J Biol Phys Chem 4(2):64–73CrossRefGoogle Scholar
  13. 13.
    Fisher J, Piterman N, Hubbard EJA, Stern MJ, Harel D (2005) Computational insights into Caenorhabditis elegans vulval development. Proc Natl Acad Sci 102(6):1951–1956CrossRefGoogle Scholar
  14. 14.
    Fisher J, Henzinger T (2007) Executable cell biology. Nat Biotechnol 25(11):1239–1249CrossRefGoogle Scholar
  15. 15.
    Giacobbe M, Guet CC, Gupta A, Henzinger TA, Paixão T, Petrov T (2015) Model checking gene regulatory networks. Lecture notes in computer science (including subseries Lecture notes in artificial intelligence and Lecture notes in bioinformatics), vol 9035, pp 469–483CrossRefGoogle Scholar
  16. 16.
    Gong H, Zuliani P, Wang Q, Clarke EM (2011) Formal analysis for logical models of pancreatic cancer. In: IEEE conference on decision and control and European control conference, pp 4855–4860Google Scholar
  17. 17.
    Guziolowski C, Videla S, Eduati F, Cokelaer T, Siegel A, Saez-rodriguez J et al (2013) Exhaustively characterizing feasible logic models of a signaling network using answer set programming. Bioinformatics 393Google Scholar
  18. 18.
    Herrmann F, Groß A, Zhou D, Kestler Ha, Kuhl M (2012) A Boolean model of the cardiac gene regulatory network determining first and second heart field identity. PLoS ONE 7(10):e46798CrossRefGoogle Scholar
  19. 19.
    Hoppe PS, Schwarzfischer M, Loeffler D, Kokkaliaris KD, Hilsenbeck O, Moritz N et al (2016) Early myeloid lineage choice is not initiated by random PU.1 to GATA1 protein ratios. Nature 535(7611):299–302CrossRefGoogle Scholar
  20. 20.
    Khalis Z, Comet JP, Richard A, Bernot G (2009) The SMBioNet method for discovering models of gene regulatory networks. Genes Genomes Genomics 3(1):15–22Google Scholar
  21. 21.
    Krumsiek J, Marr C, Schroeder T, Theis FJ (2011) Hierarchical differentiation of myeloid progenitors is encoded in the transcription factor network. PloS One 6(8):e22649CrossRefGoogle Scholar
  22. 22.
    Kugler H, Dunn SJ, Yordanov B (2018) Formal analysis of network motifs. In: Ceska M, Safranek D (eds) Computational methods in systems biology. Springer International Publishing, New York, pp 111–128Google Scholar
  23. 23.
    Kwiatkowska M, Norman G, Parker D (2010) Probabilistic model checking for systems biology. In: Iyengar MS (ed)Google Scholar
  24. 24.
    Kwiatkowska M, Norman G, Parker D (2011) PRISM 4.0: verification of probabilistic real-time systems. Formal modeling and verification of cyber-physical systems. Springer Fachmedien Wiesbaden, Wiesbaden, pp 585–591CrossRefGoogle Scholar
  25. 25.
    Kwiatkowska M, Thachuk C (2014) Probabilistic model checking for biology. Softw Syst Saf 36:165Google Scholar
  26. 26.
    Le Novère N (2015) Quantitative and logic modelling of molecular and gene networks. Nat Rev Genet 16(3):146–158CrossRefGoogle Scholar
  27. 27.
    Mishra A, Oulès B, Pisco AO, Ly T, Liakath-Ali K, Walko G et al (2017) A protein phosphatase network controls the temporal and spatial dynamics of differentiation commitment in human epidermis. Elife 6:1–20Google Scholar
  28. 28.
    Moignard V, Woodhouse S, Haghverdi L, Lilly AJ, Tanaka Y, Wilkinson AC et al (2015) Decoding the regulatory network of early blood development from single-cell gene expression measurements. Nat Biotechnol 33:269–276CrossRefGoogle Scholar
  29. 29.
    Nichols J, Smith A (2012) Pluripotency in the embryo and in culture. Cold Spring Harb Perspect Biol 4(8):a008128–a008128CrossRefGoogle Scholar
  30. 30.
    Pimanda JE, Ottersbach K, Knezevic K, Kinston S, Chan WYI, Wilson NK et al (2007) Gata2, Fli1, and Scl form a recursively wired gene-regulatory circuit during early hematopoietic development. PNAS 104(45):17692–17697CrossRefGoogle Scholar
  31. 31.
    SA Kauffman (1969) Metabolic stability and epigenesis in randomly constructed genetic nets. J Theor Biol 22(3):437–467MathSciNetCrossRefGoogle Scholar
  32. 32.
    Schaub T, Siegel A, Videla S (2014) Reasoning on the response of logical signaling networks with ASP. Logical modeling of biological systems. Wiley, Hoboken, pp 49–92Google Scholar
  33. 33.
    Shavit Y, Yordanov B, Dunn SJ, Wintersteiger CM, Otani T, Hamadi Y et al (2016) Automated synthesis and analysis of switching gene regulatory networks. BioSystems 146:26–34CrossRefGoogle Scholar
  34. 34.
    Stergachis AB, Neph S, Reynolds A, Humbert R, Miller B, Paige SL et al (2013) Developmental fate and cellular maturity encoded in human regulatory DNA landscapes. Cell 154(4):888–903CrossRefGoogle Scholar
  35. 35.
    Takahashi K, Yamanaka S (2006) Induction of pluripotent stem cells from mouse embryonic and adult fibroblast cultures by defined factors. Cell 126(4):663–676CrossRefGoogle Scholar
  36. 36.
    Videla S, Guziolowski C, Eduati F, Thiele S, Gebser M, Nicolas J et al (2015) Learning Boolean logic models of signaling networks with ASP. Theor Comput Sci 599:79–101MathSciNetzbMATHCrossRefGoogle Scholar
  37. 37.
    Wang Q, Clarke EM (2016) Formal modeling of biological systems. In: 2016 IEEE international high level design validation and test workshop (HLDVT). IEEE, pp 178–184Google Scholar
  38. 38.
    Yachie-Kinoshita A, Onishi K, Ostblom J, Langley MA, Posfai E, Rossant J et al (2018) Modeling signaling dependent pluripotency with Boolean logic to predict cell fate transitions. Mol Syst Biol 14(1):e7952CrossRefGoogle Scholar
  39. 39.
    Yordanov B, Dunn SJ, Kugler H, Smith A, Martello G, Emmott S (2016) A method to identify and analyze biological programs through automated reasoning. NPJ Syst Biol Appl 2:16010Google Scholar
  40. 40.
    Yordanov B, Wintersteiger CM, Hamadi Y, Kugler H (2013) SMT-based analysis of biological computation. In: NASA formal methods symposium, pp 78–92Google Scholar
  41. 41.
    Yosef N, Shalek AK, Gaublomme JT, Jin H, Lee Y, Awasthi A et al (2013) Dynamic regulatory network controlling TH17 cell differentiation. Nature 496(7446):461–468CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Microsoft ResearchCambridgeUK

Personalised recommendations