Model Checking Gene Regulatory Networks

TL;DR

This paper introduces a formal verification approach for gene regulatory networks, replacing traditional simulation methods with model checking to efficiently analyze mutational robustness in biological systems.

Contribution

It presents a novel parameter synthesis method using symbolic model checking and SMT solving for analyzing gene regulatory networks, improving efficiency over classical simulation techniques.

Findings

More efficient computation of mutational robustness

Formal verification provides higher assurance than simulation

Applicable to weighted gene regulatory network models

Abstract

The behaviour of gene regulatory networks (GRNs) is typically analysed using simulation-based statistical testing-like methods. In this paper, we demonstrate that we can replace this approach by a formal verification-like method that gives higher assurance and scalability. We focus on Wagner weighted GRN model with varying weights, which is used in evolutionary biology. In the model, weight parameters represent the gene interaction strength that may change due to genetic mutations. For a property of interest, we synthesise the constraints over the parameter space that represent the set of GRNs satisfying the property. We experimentally show that our parameter synthesis procedure computes the mutational robustness of GRNs -an important problem of interest in evolutionary biology- more efficiently than the classical simulation method. We specify the property in linear temporal logics. We employ symbolic bounded model checking and SMT solving to compute the space of GRNs that satisfy the property, which amounts to synthesizing a set of linear constraints on the weights.