Model Checking Cell Fate Decisions

As time goes by, it becomes more and more apparent that the puzzles of life involve more and more molecular pieces that fit together in increasingly complex ways. Biology is not an exact science. It is messy and noisy, and most often vague and ambiguous. We cannot assign clear rules to the way cells behave and interact with one another, and we often cannot quantify the exact amounts of molecules, such as genes and proteins, in the resolution of a single cell. To make matters worse (so to speak), the combinatorial complexity observed in biological networks is staggering, which renders the comprehension and analysis of such systems a major challenge. Recent efforts to create executable models of complex biological phenomena - an approach called Executable Biology - entail great promise for new scientific discoveries, shading new light on the puzzle of life. At the same time, this ’new wave of the future’ forces Computer Science to stretch far and beyond, and in ways never considered before, in order to deal with the enormous complexity observed in biology. In this talk, I will summarize some of the success stories in using formal verification to reason about mechanistic models in biology. In particular, I will focus on models of cell fate decisions during normal development, organogenesis, and cancer, and their analysis using model checking. If time permits, I will also mention some of the major milestones on the way to conquer biological complexity.