Skip to main content
SpringerLink
Log in

Temporal Logic Based Synthesis of Experimentally Constrained Interaction Networks

  • Conference paper
  • First Online:
Molecular Logic and Computational Synthetic Biology (MLCSB 2018)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 11415))

Abstract

Synthesis methods based on formal reasoning are a powerful way to automate the process of constructing computational models of gene regulatory networks (GRNs) and increase predictive power by considering a set of consistent models that are guaranteed to satisfy known experimental data. Previously, a formal reasoning based approach enabling the synthesis and analysis of biological networks formalized using Abstract Boolean Networks (ABNs) was developed, where the precise interactions and update rules are only partially known. System dynamics can be constrained with specifications of some required behaviors, thereby providing a characterization of the set of all networks capable of reproducing given experimental observations. The synthesis method is supported by a tool, the Reasoning Engine for Interaction Networks (RE:IN). Starting with the synthesis framework supported by RE:IN, we provide translations of experimental observations to temporal logic and semantics of Abstract Boolean Networks, enabling us to use off-the-shelf model checking tools and algorithms. An initial prototype implementation we have developed demonstrates this is a gainful approach, providing speed-up gains for some benchmarks, while also opening the way to study extensions of the experimental observations specification language currently supported in RE:IN by using the rich expressive power of temporal logic.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Ball, T., Levin, V., Rajamani, S.K.: A decade of software model checking with slam. Commun. ACM 54(7), 68–76 (2011)

    Article  Google Scholar 

  2. Barnat, J., Brim, L., Cerna, I., Drazan, S., Safranek, D.: From simple regulatory motifs to parallel model checking of complex transcriptional networks. In: Pre-proceedings of Parallel and Distributed Methods in Verification (PDMC 2008) Budapest, pp. 83–96 (2008)

    Google Scholar 

  3. Bartocci, E., Lió, P.: Computational modeling, formal analysis, and tools for systems biology. PLoS Comput. Biol. 12(1), e1004591 (2016)

    Article  Google Scholar 

  4. Batt, G., et al.: Validation of qualitative models of genetic regulatory networks by model checking: analysis of the nutritional stress response in Escherichia coli. Bioinformatics 21, 19–28 (2005)

    Article  Google Scholar 

  5. Chabrier, N., Fages, F.: Symbolic model checking of biochemical networks. In: Priami, C. (ed.) CMSB 2003. LNCS, vol. 2602, pp. 149–162. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-36481-1_13

    Chapter  Google Scholar 

  6. Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NUSMV: a new symbolic model checker. Int. J. Softw. Tools Technol. Transf. 2(4), 410–425 (2000)

    Article  Google Scholar 

  7. Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982). https://doi.org/10.1007/BFb0025774

    Chapter  Google Scholar 

  8. de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24

    Chapter  Google Scholar 

  9. Dubrova, E., Teslenko, M., Ming, L.: Finding attractors in synchronous multiple-valued networks using SAT-based bounded model checking. In: 40th IEEE International Symposium on Multiple-Valued Logic (ISMVL), pp. 144–149 (2010)

    Google Scholar 

  10. Dunn, S.-J., Li, M.A., Carbognin, E., Smith, A.G., Martello, G.: A common molecular logic determines embryonic stem cell self-renewal and reprogramming. bioRxiv, p. 200501 (2017)

    Google Scholar 

  11. Dunn, S.-J., Li, M.A., Carbognin, E., Smith, A.G., Martello, G.: A common molecular logic determines embryonic stem cell self-renewal and reprogramming. EMBO J. 38, e100003 (2018)

    Article  Google Scholar 

  12. Dunn, S.-J., Martello, G., Yordanov, B., Emmott, S., Smith, A.G.: Defining an essential transcription factor program for naïve pluripotency. Science 344(6188), 1156–1160 (2014)

    Article  Google Scholar 

  13. Emerson, E.A., Halpern, J.Y.: ‘Sometimes’ and ‘not never’ revisited: on branching time versus linear time. J. ACM 33, 151–178 (1986)

    Article  Google Scholar 

  14. Fisman, D., Kugler, H.: Temporal reasoning on incomplete paths. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11245, pp. 28–52. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-03421-4_3

    Chapter  Google Scholar 

  15. Fix, L.: Fifteen years of formal property verification in intel. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol. 5000, pp. 139–144. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-69850-0_8

    Chapter  MATH  Google Scholar 

  16. Friedman, N., Linial, M., Nachman, I., Pe’er, D.: Using Bayesian networks to analyze expression data. J. Comput. Biol. 3(7), 601–620 (2000)

    Article  Google Scholar 

  17. Guziolowski, C., et al.: Exhaustively characterizing feasible logic models of a signaling network using answer set programming. Bioinformatics 29(18), 2320–2326 (2013)

    Article  Google Scholar 

  18. Ito, S., Ichinose, T., Shimakawa, M., Izumi, N., Hagihara, S., Yonezaki, N.: Formal analysis of gene networks using network motifs. In: Fernández-Chimeno, M., et al. (eds.) BIOSTEC 2013. CCIS, vol. 452, pp. 131–146. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-44485-6_10

    Chapter  Google Scholar 

  19. Koksal, A.S.: Program Synthesis for Systems Biology. PhD thesis, University of California at Berkeley. Technical Report No. UCB/EECS-2018-49 (2018)

    Google Scholar 

  20. Koksal, A.S., Pu, Y., Srivastava, S., Bodik, R., Fisher, J., Piterman, N.: Synthesis of biological models from mutation experimentss. In: SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM (2013)

    Google Scholar 

  21. Kroening, D., Strichman, O.: Decision Procedures, vol. 5. Springer, Heidelberg (2008)

    MATH  Google Scholar 

  22. Kugler, H., Plock, C., Roberts, A.: Synthesizing biological theories. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 579–584. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_46

    Chapter  Google Scholar 

  23. Kugler, H., Pnueli, A., Stern, M.J., Hubbard, E.J.A.: “Don’t care” modeling: a logical framework for developing predictive system models. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 343–357. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-71209-1_27

    Chapter  MATH  Google Scholar 

  24. Kugler, H., Dunn, S.-J., Yordanov, B.: Formal analysis of network motifs. In: Češka, M., Šafránek, D. (eds.) CMSB 2018. LNCS, vol. 11095, pp. 111–128. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-99429-1_7

    Chapter  Google Scholar 

  25. Kupferman, O.: Recent challenges and ideas in temporal synthesis. In: Bieliková, M., Friedrich, G., Gottlob, G., Katzenbeisser, S., Turán, G. (eds.) SOFSEM 2012. LNCS, vol. 7147, pp. 88–98. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-27660-6_8

    Chapter  Google Scholar 

  26. Liang, S., Fuhrman, S., Somogyi, R.: Reveal, a general reverse engineering algorithm for inference of genetic network architectures. In: Pacific Symposium on Biocomputing, vol. 3, pp. 18–29. Springer (1998)

    Google Scholar 

  27. Marbach, D., Prill, R.J., Schaffter, T., Mattiussi, C., Floreano, D., Stolovitzky, D.: Revealing strengths and weaknesses of methods for gene network inference. Proc. Nat. Acad. Sci. 107(14), 6286–6291 (2010)

    Article  Google Scholar 

  28. Mishra, A., et al.: A protein phosphatase network controls the temporal and spatial dynamics of differentiation commitment in human epidermis. Elife 6, e27356 (2017)

    Article  Google Scholar 

  29. Moignard, V., et al.: Decoding the regulatory network of early blood development from single-cell gene expression measurements. Nat. Biotechnol. 33(3), 269 (2015)

    Article  Google Scholar 

  30. Paoletti, N., Yordanov, B., Hamadi, Y., Wintersteiger, C.M., Kugler, H.: Analyzing and synthesizing genomic logic functions. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 343–357. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_23

    Chapter  Google Scholar 

  31. Pnueli, A.: The temporal logic of programs. In: Proceedings of 18th IEEE Symposium on Foundations of Computer Science, pp. 46–57 (1977)

    Google Scholar 

  32. Shavit, Y., et al.: Automated synthesis and analysis of switching gene regulatory networks. Biosystems 146, 26–34 (2016)

    Article  Google Scholar 

  33. Tiwari, A., Talcott, C., Knapp, M., Lincoln, P., Laderoute, K.: Analyzing pathways using SAT-based approaches. In: Anai, H., Horimoto, K., Kutsia, T. (eds.) AB 2007. LNCS, vol. 4545, pp. 155–169. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73433-8_12

    Chapter  Google Scholar 

  34. Woodhouse, S., Piterman, N., Wintersteiger, C.M., Göttgens, B., Fisher, J.: SCNS: a graphical tool for reconstructing executable regulatory networks from single-cell genomic data. BMC Syst. Biol. 12(1), 59 (2018)

    Article  Google Scholar 

  35. Yordanov, B., Dunn, S.-J., Kugler, H., Smith, A., Martello, G., Emmott, S.: A method to identify and analyze biological programs through automated reasoning. NPJ Syst. Biol. Appl. 2, 16010 (2016)

    Article  Google Scholar 

  36. Yordanov, B., Wintersteiger, C.M., Hamadi, Y., Kugler, H.: SMT-based analysis of biological computation. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 78–92. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38088-4_6

    Chapter  Google Scholar 

Download references

Acknowledgment

The research was partially supported by the Horizon 2020 research and innovation programme for the Bio4Comp project under grant agreement number 732482. We also acknowledge the support of the program for Summer Science Research Internships for Yeshiva University Students at Bar-Ilan University.

Author information

Authors and Affiliations

  1. Yeshiva University, New York, USA

    Judah Goldfeder

  2. Bar-Ilan University, Ramat-Gan, Israel

    Hillel Kugler

Authors
  1. Judah Goldfeder
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Hillel Kugler
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Hillel Kugler .

Editor information

Editors and Affiliations

  1. Inria Sophia Antipolis - Méditerranée, Inria, Sophia Antipolis Cedex, France

    Madalena Chaves

  2. Department of Mathematics, University of Aveiro, Aveiro, Portugal

    Manuel A. Martins

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Goldfeder, J., Kugler, H. (2019). Temporal Logic Based Synthesis of Experimentally Constrained Interaction Networks. In: Chaves, M., Martins, M. (eds) Molecular Logic and Computational Synthetic Biology. MLCSB 2018. Lecture Notes in Computer Science(), vol 11415. Springer, Cham. https://doi.org/10.1007/978-3-030-19432-1_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-19432-1_6

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-19431-4

  • Online ISBN: 978-3-030-19432-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation