title: Toward synthesizing executable models in biology.
abstract: Over the last decade, executable models of biological behaviors have repeatedly provided new scientific discoveries, uncovered novel insights, and directed new experimental avenues. These models are computer programs whose execution mechanistically simulates aspects of the cell's behaviors. If the observed behavior of the program agrees with the observed biological behavior, then the program explains the phenomena. This approach has proven beneficial for gaining new biological insights and directing new experimental avenues. One advantage of this approach is that techniques for analysis of computer programs can be applied to the analysis of executable models. For example, one can confirm that a model agrees with experiments for all possible executions of the model (corresponding to all environmental conditions), even if there are a huge number of executions. Various formal methods have been adapted for this context, for example, model checking or symbolic analysis of state spaces. To avoid manual construction of executable models, one can apply synthesis, a method to produce programs automatically from high-level specifications. In the context of biological modeling, synthesis would correspond to extracting executable models from experimental data. We survey recent results about the usage of the techniques underlying synthesis of computer programs for the inference of biological models from experimental data. We describe synthesis of biological models from curated mutation experiment data, inferring network connectivity models from phosphoproteomic data, and synthesis of Boolean networks from gene expression data. While much work has been done on automated analysis of similar datasets using machine learning and artificial intelligence, using synthesis techniques provides new opportunities such as efficient computation of disambiguating experiments, as well as the ability to produce different kinds of models automatically from biological data.
authors.affiliation: Microsoft Research , Cambridge , UK ; Department of Biochemistry, University of Cambridge , Cambridge , UK.
authors.forename: Jasmin
authors.initials: J
authors.lastname: Fisher
authors.affiliation: Department of Computer Science, University of Leicester , Leicester , UK.
authors.forename: Nir
authors.initials: N
authors.lastname: Piterman
authors.affiliation: Electrical Engineering and Computer Science, University of California Berkeley , Berkeley, CA , USA.
authors.forename: Rastislav
authors.initials: R
authors.lastname: Bodik
keywords: Boolean networks; executable biology; signaling pathways; synthesis; verification