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