Analysis of genetic networks with model checking

Over the last decades, biological networks, like signal transduction pathways, metabolic pathways, and genetic networks, have received increasing attention in biochemistry. In each living organism a growing plethora of such networks have been identified. Is has become clear that the understanding of the mechanisms and their functioning is crucial for elucidating the functioning of the cell and the organism as a whole.

Different formalisms and approaches exist for the modelling of biological networks. We apply model checking as a method that exploits executable models. The main leeway of these models is that they lend themselves to formal verification. Standard simulation on the model can only yield predictions regarding model properties with certain probability. Unlike standard simulation, model checking based approaches explore all possible behaviours of the systems, not just some subset of it and therefore yield conclusions with certainty.

In contrast to the quantitative models like differential equations, Boolean models consider only two states of the network elements, i.e., their expressions – active or inactive. The advantage of such models is that are easier to analyse, than the fully quantitative ones. On the examples of genetic networks of Arabidopsis Thaliana and Fruit Fly, we show how the formal approach with model checking can reveal subtle errors in the models and that can improve predictive power of the analysis.