A Genetically Modified Hoare Logic

TL;DR

This paper introduces a novel approach using Hoare Logic and weakest precondition calculus to identify all parameter values consistent with observed gene network behaviors in a discrete framework.

Contribution

It develops a new method applying Hoare Logic to model gene networks, enabling exhaustive parameter search and providing proofs of correctness and completeness.

Findings

Successfully generates constraints on gene network parameters.

Proves the correctness of the Hoare logic approach for gene networks.

Establishes the completeness of the method via weakest precondition computation.

Abstract

An important problem when modeling gene networks lies in the identification of parameters, even if we consider a purely discrete framework as the one of Ren\'e Thomas. Here we are interested in the exhaustive search of all parameter values that are consistent with observed behaviors of the gene network. We present in this article a new approach based on Hoare Logic and on a weakest precondition calculus to generate constraints on possible parameter values. Observed behaviors play the role of "programs" for the classical Hoare logic, and computed weakest preconditions represent the sets of all compatible parameterizations expressed as constraints on parameters. Finally we give a proof of correctness of our Hoare logic for gene networks as well as a proof of completeness based on the computation of the weakest precondition.