Updates

Paper to appear in NASA Formal Methods 2013

You can try out several of the z3-4Biology examples directly from your browser in the rise4fun environment at http://rise4fun.com/Z34Biology

You can download all updated models and analysis problems, both as simple textual representations or translated into benchmarks using the SMT-LIB format. These examples include problems from the analysis of Boolean networks such as gene regulation networks and chemical reaction networks such as DNA circuits. The benchmarks are available as a package from here.

Motivation

Many of the basic principles governing the development and function of living organisms remain poorly understood, despite the significant progress in molecular and cellular biology and breakthroughs in experimental methods. The development of computational models can improve our understanding of biological systems and biological computation and help address questions like what cells compute, how do they perform computation, and in what ways can such computation be modified or engineered, for example, to allow intervening with abnormal behavior (disease) or designing computational devices using biological principles. To answer such questions, model simulation is often not sufficient and more powerful analysis methods are needed.

Inspired by the study of engineered computational systems such as computer hardware and software, the application of formal methods has recently attracted attention in the context of biological computation. However, formal methods in biology are often implemented as stand-alone tools focused on specific problems, thereby hindering the reproducibility of results and the collaborative improvement of the procedures.

Here, we make available a collection of biological models from a variety of areas including gene regulation and signalling networks, developmental biology, synthetic biology and DNA computing. Despite the various formalisms used initially to construct these models, here they are encoded using a unified representation, allowing their analysis using SMT solvers such as Z3. The richness of the SMT problem can accommodate procedures to address a diverse set of biological questions. We demonstrate potential application through several procedures (also made available on this web site), which include system stability analysis, identification of gene knockouts and verification of a type of DNA computing circuits.

Model structure and file format

All models and analysis procedures are made available in the SMT-LIB format (as plain text files). Currently, the models are constructed using quantified bit-vectors, which are supported by the Z3 solver (to the best of our knowledge Z3 is currently the only solver which supports the UFBV logic). A convenient way to get started is to use the online version of the Z3 solver available here. To do so, simply copy the SMT description of a model or procedure of interest from the appropriate file, paste it into the Z3 solver and press "ask Z3". Note that there are some limitations to the online version of Z3.

Boolean Networks

Chemical Reaction Networks

DNA Transducer gate cascade

Scenario-based Models

C. elegans vulval cell fate specification model (VPC)

Gene circuits

Simple gene circuit design problem