#
Using Hoare logic for constraining parameters of discrete models of
gene networks

### Keywords:

Discrete modelling,
Biological regulatory networks,
formal methods,
constraints programming.
### Abstract:

The technology of DNA chips allows the
quantification of the expression level of thousands genes in the same
organism at the same time. Nevertheless, analysis of data from DNA
chips requires development of adapted methods.
We propose a path language that allows the description, in an abstract
way, of the concentration level variations from temporal data like
temporal profiles of gene expression. When concentration level
variations have been expressed through a program of the path language,
it becomes possible to apply methods from computer science like Hoare
logic.

Hoare logic is made of a system composed of axioms and rules. It
permits one to prove if a program is correct in comparison to its
specifications that is described through assertions, that is, logical
formulas, that define properties on the program. The precondition
specifies the initial state before the execution of the program and
the postcondition specifies the final state after the execution of the
program. A program is said (partially) correct if it is possible to
prove that from an initial state satisfying the precondition, the
program leads (if the program terminates) to a final state satisfying
the postcondition.

To model gene regulatory networks, the main difficulty remains in the
parameter identification problem, that is, the search of parameter
values which lead to a model behavior that is consistent with the
known or hypothetical properties of the system. So, we apply a
Hoare-like logic designed for the defined path language. The axioms
and rules of this Hoare-like logic are adapted to gene networks and
permits us to prove that the path described by the program exists in
the dynamics. Given a path program and a postcondition, we can apply
calculus of the weakest precondition, based on this Hoare-like
logic. Calculus of the weakest precondition, thanks to defined axioms
and rules, permits us to constrain parameters associated with the
program and the postcondition. Although Hoare logic is well known, its
application to constrain parameter values of gene networks appears to
be brand new and helpful in order to select consistent
models. Moreover, expressing DNA profiles into programs gives another
way to process such data.

**Address:**
Lab. I3S, UMR 6070 UNS and CNRS, Algorithmes-Euclide-B,
2000 route des Lucioles, B.P. 121, F-06903, Sophia-Antipolis, France

**Authors: **

Zohra Khalis khalis@i3s.unice.fr university of Nice Sophia Antipolis

Gilles Bernot bernot@unice.fr University of Nice Sophia Antipolis

Jean-Paul Comet comet@unice.fr University de Nice Sophia Antipolis