La compréhension de la dynamique des forêts tropicales hyperdiverses a toujours été un défi en écologie. Historiquement les modèles se basant sur le concept de la niche ou la courbe logistique ont montré leurs limites lorsqu'il s'agissait d'expliquer la diversité d'espèces en forêt tropicale. L'arrivée des modèles neutres en écologie a permis d'exprimer dans un cadre mathématique l'échantillonnage des forêts tropicales, ouvrant de nouvelles perspectives. Ces modèles, très réduits en nombre de paramètres, ont été développés depuis la génétique des populations. Encore peu explorés, ces modèles considèrent les espèces comme étant fonctionnellement équivalentes entre elles. Pour commencer, nous réexaminerons les avancées récentes dans ce domaine extrêmement actif, pour discuter ensuite du développement futur de ces modèles. Dans un second temps, nous analyserons l'inférence des paramètres neutres, afin d'établir ce lien important entre modèles théoriques et données du terrain. De plus, nous introduirons un nouvel estimateur du paramètre décrivant la richesse d'espèces rencontrées dans ces forêts. Ces résultats seront mis en perspective par l'utilisation des données de terrain provenant des forêts sempervirentes des Ghâts Occidentaux d'Inde ainsi que des forêts humides autour du Canal du Panama. Nous testerons également ces approches sur des simulations variées. Finalement, nous essayerons d'évaluer la pertinence des estimations du paramètre de migration en les comparant avec les distances de dispersion des graines observées en forêt tropicale. / Understanding the dynamics of highly diverse communities such as tropical forests has always been a challenging task in ecology. Historically, simplified logistic models and complex niche theories have had a limited success in explaining the species diversity and composition in a tropical context. With the advent of neutral models, we have an original quantitative framework in terms of a sampling theory which opens new perspectives in the field of tropical community ecology. These parsimonious models originally developed from existing theories in population genetics, have a highly selective interpretation of niche theory defined as the functional equivalence of species which has been insufficiently explored. To begin with, we review recent advances of this extremely active field and provide insights into future developments of this theory. Further on, we provide a detailed account of parameter inference which is the crucial link between theoret ical models and field data. In addition, we improve on existing approaches by introducing a novel estimator for the parameter explaining the species richness found in these forests. These results are put into perspective by using field data from the wet evergreen forests of the Western Ghats region of India and the tropical rain forests around the Panama Canal Watershed. Our results are also rigorously tested using simulations of neutral community composition. Lastly, we provide insights into whether parameter inferences dealing with immigration correspond to the seed dispersal distances typically found in tropical forests.

Les progrès récents des techniques expérimentales biologiques ont conduit à la production d'une énorme quantité de données sur le comportement dynamique des réseaux de régulation génique (RRG). Nous présentons une approche pour l'identification des modèles affines-par-morceaux (APM) de RRGs à partir de données expérimentales. Ces modèles reposent sur l'hypothèse que la régulation survient au niveau de la synthèse et de la dégradation des produits de l'expression des gènes : les paramètres cinétiques sont supposés être constants jusqu'à ce que la concentration d'une protéine régulatrice franchisse un seuil de transition.<br /><br />La méthode que nous présentons se concentrent sur le problème de la détection des transitions entre les différents modes dynamiques à partir des données d'expression génique et sur la reconstruction des seuils de transition associés avec les interactions régulatrices. En particulier, notre méthode prend en considération les contraintes géométriques spécifiques aux modèles APM de RRGs. Une telle méthode d'identification est conçue pour des systèmes à erreur sur la sortie où les observations sont des séries temporelles de mesures bruitées de niveaux de concentration à l'intérieur d'une cellule.<br /><br />Les données sont d'abord classées en modes dans lesquels le comportement dynamique est considéré comme étant complètement décrit par une équation différentielle linéaire. À partir de la classification résultante, une technique de reconnaissance de forme est utilisée pour reconstruire toutes les combinaisons de seuils de transition qui sont cohérentes avec les données mesurées. Pour chaque combinaison de seuils, il est alors possible de fournir un réseau de régulation et les paramètres dynamiques de chaque mode.<br /><br />Les performances de notre approche ont été analysées en utilisant des données artificielles simulées pour un modèle simplifié de la réponse à un manque de carbone pour le bactérie Escherichia coli. En particulier, nous avons évalué l'influence du niveau du bruit et du pas d'échantillonnage sur les systèmes identifiés. Nos résultats montrent que la méthode, en association avec des séries temporelles de mesures suffisamment précises, lesquelles peuvent être obtenues avec des systèmes à gène rapporteur, permettent une identification quantitative de modèles APM de RRGs.

Dans ce mémoire, nous présentons l’utilisation de techniques de model-checking pour l’inférence de paramètres de réseaux de régulation génétique (GRN) et l’analyse formelle d’une voie de signalisation. Le coeur du mémoire est décrit dans la première partie, dans laquelle nous proposons une approche pour inférer les paramètres biologiques régissant les dynamiques de modèles discrets de GRN. Les GRN sont encodés sous la forme d’un méta-modèle, appelé GRN paramétré, de telle façon qu’une instance de paramètres définit un modèle discret du GRN initial. Sous réserve que les propriétés biologiques d’intérêt s’expriment sous la forme de formules LTL, les techniques de model-checking LTL sont combinées à celles d’exécution symbolique et de résolution de contraintes afin de sélectionner les modèles satisfaisant ces propriétés. L’enjeu est de contourner l’explosion combinatoire en terme de taille et de nombre de modèles discrets. Nous avons implémenté notre méthode en Java, dans un outil appelé SPuTNIk. La seconde partie décrit une collaboration avec des neuropédiatres, qui ont pour objectif de comprendre l’apparition du phénotype protecteur ou toxique des microglies (un type de macrophage du cerveau) chez les prématurés. Cette partie exploite un autre versant du model-checking, celui du modelchecking statistique, afin d’étudier un type de réseau biologique particulier : la voie de signalisation Wnt/β-caténine, qui permet la transmission d’un signal de l’extérieur à l’intérieur des cellules via une cascade de réactions biochimiques. Nous présentons ici l’apport du model-checker stochastique COSMOS, utilisant la logique stochastique à automate hybride (HASL), un formalisme très expressif nous permettant une analyse formelle sophistiquée des dynamiques de la voie Wnt/β-caténine, modélisée sous la forme d’un processus stochastique à événements discrets. / In this thesis, we present the use of model checking techniques for inference of parameters of Gene Regulatory Networks (GRNs) and formal analysis of a signalling pathway. In the first and main part, we provide an approach to infer biological parameters governing the dynamics of discrete models of GRNs. GRNs are encoded in the form of a meta-model, called Parametric GRN, such that a parameter instance defines a discrete model of the original GRN. Provided that targeted biological properties are expressed in the form of LTL formulas, LTL model-checking techniques are combined with symbolic execution and constraint solving techniques to select discrete models satisfying these properties. The challenge is to prevent combinatorial explosion in terms of size and number of discrete models. Our method is implemented in Java, in a tool called SPuTNIk. The second part describes a work performed in collaboration with child neurologists, who aim to understand the occurrence of toxic or protective phenotype of microglia (a type of macrophage in the brain) in the case of preemies. We use an other type of model-checking, the statistical model-checking, to study a particular type of biological network: the Wnt/β- catenin pathway that transmits an external signal into the cells via a cascade of biochemical reactions. Here we present the benefit of the stochastic model checker COSMOS, using the Hybrid Automata Stochastic Logic (HASL), that is an very expressive formalism allowing a sophisticated formal analysis of the dynamics of the Wnt/β-catenin pathway, modelled as a discrete event stochastic process.