A Hybrid Hoare Logic for Gene Network Models

TL;DR

This paper introduces a hybrid Hoare logic framework for gene network models with continuous time, enabling the derivation of parameter constraints from biological data using formal verification techniques.

Contribution

It presents a novel hybrid automata-based approach combined with Hoare logic and weakest precondition calculus for parameter constraint generation in continuous-time gene network models.

Findings

Successfully applied to lacI repressor model

Generated meaningful parameter constraints from biological traces

Demonstrated the approach's potential for biological model analysis

Abstract

The main difficulty when modelling gene networks is the identification of the parameters that govern their dynamics. It is particularly difficult for models in which time is continuous: parameters have real values which cannot be enumerated. The widespread idea is to infer new constraints that reduce the range of possible values. Here we present a new work based on a particular class of Hybrid automata (inspired by Thomas discrete models) where discrete parameters are replaced by signed celerities. We propose a new approach involving Hoare logic and weakest precondition calculus (a la Dijkstra) that generates constraints on the parameter values. Indeed, once proper specifications are extracted from biological traces with duration information (found in the literature or biological experiments), they play a role similar to imperative programs in the classical Hoare logic. We illustrate our hybrid Hoare logic on a small model controlling the lacI repressor of the lactose operon.