Friday, April 12, 2013
Speaker: Nir Piterman
Venue: IST Austria
Friday 15:00 - 16:00
In this talk I will describe a technique to synthesize models representing certain biological phenomena from specification given by mutation experiments.
The synthesis algorithm had to address two conceptual problems.
First, 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, how to 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.
If time permits, I will briefly describe our modeling language (embedded into Scala) and how this language design and embedding allows us to build an efficient synthesizer.