A genetically modified Hoare logic that identifies the parameters of a gene network,

The main difficulty when modelling gene networks is the identification of the parameters that govern the dynamics. Here we present a new approach based on Hoare logic and weakest preconditions (a la Dijkstra) that generates constraints on the parameter values: Once proper specifications are extracted from biological traces, they play a role similar to programs in the classical Hoare logic. We firstly remind the discrete modelling for genetic networks defined by René Thomas. Then, we define the Hoare/Dijkstra method extended to gene networks, that extracts the weakest precondition on parameter values.