Computational Modeling, Formal Analysis, and Tools for Systems Biology

Abstract

As the amount of biological data in the public domain grows, so does the range of modeling and analysis techniques employed in systems biology. In recent years, a number of theoretical computer science developments have enabled modeling methodology to keep pace. The growing interest in systems biology in executable models and their analysis has necessitated the borrowing of terms and methods from computer science, such as formal analysis, model checking, static analysis, and runtime verification. Here, we discuss the most important and exciting computational methods and tools currently available to systems biologists. We believe that a deeper understanding of the concepts and theory highlighted in this review will produce better software practice, improved investigation of complex biological processes, and even new ideas and better feedback into computer science.

Fig 1. Most relevant examples of computational modeling approaches introduced with toy examples.

Related tools are listed in Table 1. References for the examples are as follows: process algebras [12], compartment-based systems [21], rule-based systems [22], statecharts [23], hybrid systems [24], Boolean networks [25], Petri nets [26], agent-based models [27], lattice-based models [28].

Fig 2. Examples of temporal logics.

Comparison between the main features of the LTL (left) and Signal Temporal Logic (STL) (right) in terms of syntax (top), operators (middle), and semantics (bottom); the black circles represents a propositional state, and the arrows represent the next step in time.

Fig 3. Summary of the features for the selected tools.

Tools are classified by the supported computational modeling language, their execution semantics, and the formal analysis that can be performed, based on the literature.