Formal characterization and efficient verification of a biological robustness property

TL;DR

This paper introduces a formal framework for analyzing initial concentration robustness in chemical reaction networks, providing a more efficient verification method for monotonic networks by reducing computational effort.

Contribution

It characterizes initial concentration robustness within an existing logical framework and offers a significant reduction in the number of traces needed for verification in monotonic networks.

Findings

Characterization of initial concentration robustness in LTL framework.

Reduction in computational effort for monotonic networks.

Verification method requiring fewer traces.

Abstract

Robustness is an observable property for which a chemical reaction network (CRN) can maintain its functionalities despite the influence of different perturbations. In general, to verify whether a network is robust, it is necessary to consider all the possible parameter configurations. This is a process that can entail a massive computational effort. In the work of Rizk et al., the authors propose a definition of robustness in linear temporal logic (LTL) through which, on the basis of multiple numerical timed traces obtained by considering different parameter configurations, they verify the robustness of a reaction network. In this paper, we focus on a notion of initial concentration robustness ($\alpha$-robustness), which is related to the influence of the perturbation of the initial concentration of one species (i.e., the input) on the concentration of another species (i.e., the output) at the steady state. We characterize this notion of robustness in the framework proposed by Rizk et al., and we show that, for monotonic reaction networks, this allows us to drastically reduce the number of traces necessary to verify robustness of the CRN.