Z3-4Biology SMT-Based Analysis of Biological Computation

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 the tremendous breakthroughs in experimental methods, which allow the precise measurement and observations of the underlying biological processes. The development of system-level, mechanistic, computational models has the potential to become an indispensable foundation and tool for improving our understanding of biological systems, enabling the integration of different processes into coherent and rigorous representations that can be simulated or analyzed and whose outcomes can be compared to laboratory data and used to guide experimental work.

An intriguing property of biological systems is their ability to perform computation using information processing mechanisms and thus ensuring robust development and survival under different environments. Computational modeling has the potential to lay a foundational theory for this inherent it biological computation, allowing the study of 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 that can lead to disease or to design computational devices using biological principles.

Inspired by the study of other computational systems, the application of formal methods has recently attracted attention in the context of biology as a strategy for automatic analysis from rich specifications, leading to rigorously defined modeling languages that can be analyzed systematically and efficiently, enabling proving of system properties and not relying only on simulation. However, such methods are often implemented as stand-alone tools focused on specific problems, thereby hindering the reproducibility of results and the collaborative improvement of methods.

Here we focus on several widely used formalisms for modeling biological systems and describe how they can be encoded to allow analysis using Satisfiability Modulo Theories (SMT) based methods. This leads to a framework that is expressive (can capture a variety of formalisms and specifications), scalable (can handle models of practical interest) and extensible (additional models and analysis procedures can be integrated). We implement the proposed translation procedures for the considered model classes, produce an initial repository of models of genetic and signaling networks, developmental systems and DNA computing circuits and demonstrate several analysis procedures for challenging examples.

We share all models and specifications from this study on our web site using the popular SMT-LIB format, which allows a number of SMT solvers to be used on the same problems. In this paper we focus on presenting results from the application of the Z3 solver, which provides an interactive online environment, where the available models and analysis procedures can be explored or novel ones can be developed and tested. By making our work accessible, we hope to stimulate interdisciplinary research on the application of formal methods in biology allowing better understanding of the computational processes within living organisms.