Executable biology presents new challenges to formal systems.
This paper addresses two problems that cell biologists face when
developing formally analyzable models.
First, we show how to automatically synthesize an in-silico
model for cell development given in-vivo experiments of how particular mutation experiments influence the cell fate. The problem of synthesis under mutations is unique because mutation experiments may have non-deterministic outcomes (presumably due to races between competing signaling pathways in the cells) and the synthesized model must be able to replay all these outcomes or else the model does not faithfully describe the desired cellular processes. (In contrast, a ”regular” concurrent program synthesized under a permissive specification need not exhibit all allowed behaviors.) We developed synthesis algorithms and synthesized a model of cell fate determination in the development of earthworm C. elegans. A former version of this model previously took systems biologists months to develop.
Second, we address the problem of under-constrained specifications
that arise due to missing mutation experiments which results
in multiple models explaining the same phenomenon. This corresponds
to analyzing the space of plausible models, i.e., models that
can be synthesized under given specifications. We develop algorithms for exploring ambiguity in specifications, i.e., whether there exist alternative models that would produce different fates on some unperformed experiment. Using the algorithm, we show that for our C. elegans case study, two observationally equivalent models with same fates but with different protein interactions can be inferred. One of these was previously unknown to biologists.
In addition to posing the synthesis and ambiguity testing problems
and developing algorithms, 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.