Model Checking of Biological Systems

The goal of computational systems biology is to develop models that can predict and explain uknown facts about the dynamics of biological systems, especially, non-trivial behaviour emerging from the interplay among the enormous number of individual biochemical components. The models are based on known first principles, wet-lab measurements, and existing hypotheses available in literature. A lot of information remains unknown, e.g., quantitative parameters such as rates of individual biochemical events.

All the known or expected biological facts can be formalized in temporal logics. Model checking techniques known from formal verification can be then used to explore models with respect to a given set of temporal properties (dynamical constraints). The space of uncertainty in models can be then restricted by means of these constraints. This gives the modellers a powerful alternative to traditional parameter fitting methods.

In this talk, an overview of applications of model checking to biological models will be given. In particular, we will focus on deterministic models -- traditional differential (kinetic) models and their discrete abstractions. Two case studies of applying model checking to biological systems will be presented, in particular, gene regulation of mammalian cell cycle and ammonium transport in E. coli.