Nicola Paoletti, Boyan Yordanov, Youssef Hamadi, Christoph M. Wintersteiger, and Hillel Kugler
Deciphering the developmental program of an embryo is a fundamental question in biology. Landmark papers [9,10] have recently shown how computational models of gene regulatory networks provide system-level causal understanding of the developmental processes of the sea urchin, and enable powerful predictive capabilities. A crucial aspect of the work is empirically deriving plausible models that explain all the known experimental data, a task that becomes infeasible in practice due to the inherent complexity of the biological systems. We present a generic Satisﬁability Modulo Theories based approach to analyze and synthesize data constrained models. We apply our approach to the sea urchin embryo, and successfully improve the state-of-the-art by synthesizing, for the ﬁrst time, models that explain all the experimental observations in . A strength of the proposed approach is the combination of accurate synthesis procedures for deriving biologically plausible models with the ability to prove inconsistency results, showing that for a given set of experiments and possible class of models no solution exists, and thus enabling practical refutation of biological models.