skip to main content
10.1145/2429069.2429125acmconferencesArticle/Chapter ViewAbstractPublication PagespoplConference Proceedingsconference-collections
research-article

Synthesis of biological models from mutation experiments

Published: 23 January 2013 Publication History

Abstract

Executable biology presents new challenges to formal methods. This paper addresses two problems that cell biologists face when developing formally analyzable models.
First, we show how to automatically synthesize a concurrent in-silico model for cell development given in-vivo experiments of how particular mutations influence the experiment outcome. The problem of synthesis under mutations is unique because mutations may produce non-deterministic outcomes (presumably by introducing races between competing signaling pathways in the cells) and the synthesized model must be able to replay all these outcomes in order to faithfully describe the modeled cellular processes. In contrast, a "regular" concurrent program is correct if it picks any outcome allowed by the non-deterministic specification. We developed synthesis algorithms and synthesized a model of cell fate determination of the earthworm C. elegans. A version of this model previously took systems biologists months to develop.
Second, we address the problem of under-constrained specifications that arise due to incomplete sets of mutation experiments. Under-constrained specifications give rise to distinct models, each explaining the same phenomenon differently. Addressing the ambiguity of specifications corresponds to analyzing the space of plausible models. We develop algorithms for detecting ambiguity in specifications, i.e., whether there exist alternative models that would produce different fates on some unperformed experiment, and for removing redundancy from specifications, i.e., computing minimal non-ambiguous specifications.
Additionally, we develop a modeling language and embed it into Scala. We describe how this language design and embedding allows us to build an efficient synthesizer. For our C. elegans case study, we infer two observationally equivalent models expressing different biological hypotheses through different protein interactions. One of these hypotheses was previously unknown to biologists.

References

[1]
Rajeev Alur and Thomas A. Henzinger. Reactive modules. Formal Methods in System Design, 15(1):7--48, 1999.
[2]
A. Arkin, J. Ross, and H. H. McAdams. Stochastic kinetic analysis of developmental pathway bifurcation in phage lambda-infected Escherichia coli cells. Genetics, 149(4):1633--1648, Aug 1998.
[3]
Anil Aswani, Soile V. E. Keränen, James Brown, Charless C. Fowlkes, David W. Knowles, Mark D. Biggin, Peter Bickel, and Claire J. Tomlin. Nonparametric identification of regulatory interactions from spatial and temporal gene expression data. BMC Bioinformatics, 11:413, 2010.
[4]
Nathan A. Barker, Chris J. Myers, and Hiroyuki Kuwahara. Learning genetic regulatory network connectivity from time series data. IEEE/ACM Trans. Comput. Biology Bioinform., 8(1):152--165, 2011.
[5]
Grégory Batt, Calin Belta, and Ron Weiss. Temporal logic analysis of gene networks under parameter uncertainty. IEEE Transactions of Automatic Control, page 2008.
[6]
Gregory Batt, Delphine Ropers, Hidde de Jong, Johannes Geiselmann, Radu Mateescu, Michel Page, and Dominique Schneider. Analysis and verification of qualitative models of genetic regulatory networks: A model-checking approach. In IJCAI, 2005.
[7]
Nathalie Chabrier and François Fages. Symbolic model checking of biochemical networks. CMSB '03, 2003.
[8]
C. Chaouiya. Petri net modelling of biological networks. Brief. Bioinformatics, 8(4):210--219, Jul 2007.
[9]
Vincent Danos, Jéróme Feret, Walter Fontana, and Jean Krivine. Abstract interpretation of cellular signalling networks. VMCAI'08, pages 83--97.
[10]
Leonardo de Moura and Nikolaj Bjørner. Z3: Efficient SMT solver. In TACAS'08: Tools and Algorithms for the Construction and Analysis of Systems, volume 4963/2008 of Lecture Notes in Computer Science, pages 337--340, 2008.
[11]
David L. Dill. Model checking cell biology. In CAV, page 2, 2012.
[12]
J. Fisher, N. Piterman, A. Hajnal, and T. A. Henzinger. Predictive modeling of signaling crosstalk during C. elegans vulval development. PLoS Comput. Biol., 3(5):e92, May 2007.
[13]
Jasmin Fisher, David Harel, and Thomas A. Henzinger. Biology as reactivity. Commun. ACM, 54(10):72--82, 2011.
[14]
Jasmin Fisher and Thomas A. Henzinger. Executable cell biology. Nature Biotechnology, 25(11):1239--1249, November 2007.
[15]
Jasmin Fisher, Thomas A. Henzinger, Maria Mateescu, and Nir Piterman. Bounded asynchrony: Concurrency for modeling cell-cell interactions. In FMSB, pages 17--32, 2008.
[16]
https://oeis.org/A000670.
[17]
Sumit Gulwani. Automating string processing in spreadsheets using input-output examples. In Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, POPL '11, pages 317--330. ACM.
[18]
J. Heath, M. Kwiatkowska, G. Norman, D. Parker, and O. Tymchyshyn. Probabilistic model checking of complex biological pathways. Theoretical Computer Science, 319(3):239--257, 2008.
[19]
Na'aman Kam, Irun R. Cohen, and David Harel. The immune system as a reactive system: Modeling t cell activation with statecharts. In HCC, pages 15--22, 2001.
[20]
Na'aman Kam, David Harel, Hillel Kugler, Rami Marelly, Amir Pnueli, E. Jane Albert Hubbard, and Michael J. Stern. Formal modeling of c. elegans development: A scenario-based approach. In CMSB, pages 4--20, 2003.
[21]
http://www.cs.berkeley.edu/~koksal/.
[22]
Ali Sinan Köksal, Viktor Kuncak, and Philippe Suter. Scala to the Power of Z3: Integrating SMT and Programming. In CADE, pages 400--406, 2011.
[23]
S. Li, S. M. Assmann, and R. Albert. Predicting essential components of signal transduction networks: a dynamic model of guard cell abscisic acid signaling. PLoS Biol., 4(10):e312, Oct 2006.
[24]
H. H. McAdams and A. Arkin. Stochastic mechanisms in gene expression. Proc. Natl. Acad. Sci. U.S.A., 94(3):814--819, Feb 1997.
[25]
Martin Odersky, Lex Spoon, and Bill Venners. Programming in Scala: a comprehensive step-by-step guide. Artima Press, 2008.
[26]
Aviv Regev and Ehud Shapiro. The pi-calculus as an abstraction for biomolecular systems. 2004.
[27]
Aurélien Rizk, Grégory Batt, Francóis Fages, and Sylvain Soliman. Continuous valuations of temporal logic specifications with applications to parameter optimization and robustness measures. Theor. Comput. Sci., 412(26):2827--2839, 2011.
[28]
Armando Solar-Lezama, Christopher Grant Jones, and Rastislav Bodik. Sketching concurrent data structures. In Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation, PLDI '08, pages 136--148. ACM.
[29]
Armando Solar-Lezama, Liviu Tancau, Rastislav Bodik, Sanjit Seshia, and Vijay Saraswat. Combinatorial sketching for finite programs. In ASPLOS-XII, pages 404--415, New York, NY, USA, 2006. ACM.
[30]
Saurabh Srivastava, Sumit Gulwani, and Jeffrey S. Foster. From program verification to program synthesis. In POPL, 2010.
[31]
Martin Vechev and Eran Yahav. Deriving linearizable fine-grained concurrent objects. SIGPLAN Not., 43(6):125--135, June 2008.
[32]
A. S. Yoo, C. Bais, and I. Greenwald. Crosstalk between the EGFR and LIN-12/Notch pathways in C. elegans vulval development. Science, 303(5658):663--666, Jan 2004.

Cited By

View all
  • (2023)Combining Functional and Automata Synthesis to Discover Causal Reactive ProgramsProceedings of the ACM on Programming Languages10.1145/35712497:POPL(1628-1658)Online publication date: 11-Jan-2023
  • (2023)The Reasoning Engine: A Satisfiability Modulo Theories-Based Framework for Reasoning About Discrete Biological ModelsJournal of Computational Biology10.1089/cmb.2023.011730:9(1046-1058)Online publication date: 1-Sep-2023
  • (2022)An SMT-Based Framework for Reasoning About Discrete Biological ModelsBioinformatics Research and Applications10.1007/978-3-031-23198-8_11(114-125)Online publication date: 14-Nov-2022
  • Show More Cited By

Index Terms

  1. Synthesis of biological models from mutation experiments

      Recommendations

      Comments

      Information & Contributors

      Information

      Published In

      cover image ACM Conferences
      POPL '13: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
      January 2013
      586 pages
      ISBN:9781450318327
      DOI:10.1145/2429069
      • cover image ACM SIGPLAN Notices
        ACM SIGPLAN Notices  Volume 48, Issue 1
        POPL '13
        January 2013
        561 pages
        ISSN:0362-1340
        EISSN:1558-1160
        DOI:10.1145/2480359
        Issue’s Table of Contents
      Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

      Sponsors

      In-Cooperation

      Publisher

      Association for Computing Machinery

      New York, NY, United States

      Publication History

      Published: 23 January 2013

      Permissions

      Request permissions for this article.

      Check for updates

      Author Tags

      1. executable biology
      2. program synthesis
      3. specification ambiguity analysis

      Qualifiers

      • Research-article

      Conference

      POPL '13
      Sponsor:

      Acceptance Rates

      Overall Acceptance Rate 860 of 4,328 submissions, 20%

      Upcoming Conference

      POPL '26

      Contributors

      Other Metrics

      Bibliometrics & Citations

      Bibliometrics

      Article Metrics

      • Downloads (Last 12 months)11
      • Downloads (Last 6 weeks)0
      Reflects downloads up to 19 Feb 2025

      Other Metrics

      Citations

      Cited By

      View all
      • (2023)Combining Functional and Automata Synthesis to Discover Causal Reactive ProgramsProceedings of the ACM on Programming Languages10.1145/35712497:POPL(1628-1658)Online publication date: 11-Jan-2023
      • (2023)The Reasoning Engine: A Satisfiability Modulo Theories-Based Framework for Reasoning About Discrete Biological ModelsJournal of Computational Biology10.1089/cmb.2023.011730:9(1046-1058)Online publication date: 1-Sep-2023
      • (2022)An SMT-Based Framework for Reasoning About Discrete Biological ModelsBioinformatics Research and Applications10.1007/978-3-031-23198-8_11(114-125)Online publication date: 14-Nov-2022
      • (2019)PuddleProceedings of the Twenty-Fourth International Conference on Architectural Support for Programming Languages and Operating Systems10.1145/3297858.3304027(183-197)Online publication date: 4-Apr-2019
      • (2019)A formal methods approach to predicting new features of the eukaryotic vesicle traffic systemActa Informatica10.1007/s00236-019-00357-3Online publication date: 2-Dec-2019
      • (2019)BRE:IN - A Backend for Reasoning About Interaction Networks with Temporal LogicComputational Methods in Systems Biology10.1007/978-3-030-31304-3_15(289-295)Online publication date: 17-Sep-2019
      • (2019)Temporal Logic Based Synthesis of Experimentally Constrained Interaction NetworksMolecular Logic and Computational Synthetic Biology10.1007/978-3-030-19432-1_6(89-104)Online publication date: 28-Apr-2019
      • (2018)InverseCSGACM Transactions on Graphics10.1145/3272127.327500637:6(1-16)Online publication date: 4-Dec-2018
      • (2017)Modeling Delayed Dynamics in Biological Regulatory Networks from Time Series DataAlgorithms10.3390/a1001000810:1(8)Online publication date: 9-Jan-2017
      • (2017)Syntax-Guided Optimal Synthesis for Chemical Reaction NetworksComputer Aided Verification10.1007/978-3-319-63390-9_20(375-395)Online publication date: 13-Jul-2017
      • Show More Cited By

      View Options

      Login options

      View options

      PDF

      View or Download as a PDF file.

      PDF

      eReader

      View online with eReader.

      eReader

      Figures

      Tables

      Media

      Share

      Share

      Share this Publication link

      Share on social media