26 mars 2018
Maxime FOLSCHETTE (IRISA & IRSET)In order to avoid the inherent complexity of differential equation systems, Kauffman (1969) and Thomas (1973) built the basis of a discrete modeling relying on graphs, and which dynamics is a restriction of synchronous automata networks, while ensuring a consistence with the biological systems modeled. New problems then arise such as the automation of the process of creating such discrete or hybrid models, and the analysis of their dynamics. During this talk, after a reminder of the classical Thomas modeling, which is the basis of my works, I will present the two main aspects of my research.
* First, model completion consists in inferring the missing topology or parameters of a model.
– A first approach consisted in using a modified Hoare logic in order to find the value of some dynamical parameters in a hybrid context ; for this, a dynamical biological behavior found in the literature can be expressed as an imperative program and submitted to a weakest precondition calculus, à la Dijkstra.
– Another more recent and experimental approach consists in reconstructing the topology of a networks (especially all the influences between components) by exploiting directly expression data, contrary to existing methods that require a discretization phase beforehand.
* The second aspect is the analysis of the dynamics of such a complex system.
– Analysis with Answer Set Programming (ASP) which is a recent logic programming paradigm for which powerful solvers exist : they show good performances on several classical problems : state reachability, fixed points enumeration and complex attractors enumeration.
– Analysis with µ-calculus, which is an extension of classical temporal logic CTL* : being more expressive, it allows for instance to search for attractors of disruptions, or check models bisimulation.
– Analysis by static analysis with abstract interpretation : this approach, on the other hand, focuses on a single property (here, reachability) but considerably drops the complexity, allowing to obtain results on big models in very little time.