Les logiques modales sont des logiques permettant la représentation et l'inférence de connaissances. La logique hybride est une extension de la logique modale de base contenant des nominaux, permettant de faire référence à un unique individu ou monde du modèle. Dans cette thèse nous présentons plusieurs algorithmes de tableaux pour logiques hybrides expressives. Nous présentons aussi une implémentation de ces calculs, et nous décrivons les tests de correction et de performance que nous avons effectués, ainsi que les outils les permettant. De plus, nous étudions en détail une famille particulière de logiques liée aux logiques hybrides : les logiques avec opérateurs de comptage. Nous étudions la complexité et la décidabilité de certains de ces langages / Modal logics are logics enabling representing and inferring knowledge. Hybrid logic is an extension of the basic modal logic that contains nominals which enable to refer to a single individual or world of the model. In this thesis, we present several tableaux-based algorithms for expressive hybrid logics. We also present an implementation of these calculi and we describe correctness and performance tests we carried out, and the tools that enable these. Moreover, we study a particular family of logics related to hybrid logics: logics with counting operators.We investigate previous results, and study the complexity and decidability of certain of these languages

Nous introduisons la stratégie de réécriture de termes k-bornée (bo(k), pour k entier) pour les systèmes linéaires. Cette stratégie est associée à une classe de systèmes dits k-bornés LBO(k). Nous démontrons que les systèmes de la classe LBO (union des LBO(k) pour tous les k), inversent-préservent la reconnaissabilité. Nous montrons que les différents problèmes de terminaison et d'inverse-terminaison pour la stratégie bo(k) sont décidables et utilisons ce résultat pour démontrer la décidabilité de ces problèmes pour des sous-classes de LBO: les classes de systèmes linéaires fortement k-bornés: LFBO(k). La classe LFBO (union des LFBO(k)) inclut strictement de nombreuses classes de systèmes connues: les systèmes inverses basiques à gauche, linéaires growing, et linéaires inverses Finite-Path-Overlapping. Le problème de l'appartenance à LFBO(k) est décidable alors qu'il ne l'est pas pour LBO(0). Pour les mots, nous prouvons que la stratégie bo(k) préserve l'algébricité. Nous étendons la notion de réécriture k-bornée aux systèmes de réécriture de termes linéaires à gauche. Comme dans le cas linéaire, nous associons à cette stratégie la classe des systèmes linéaires à gauche k-bornés BO(k) qui étend la classe LBO(k). Nous démontrons que les systèmes de cette classe inverse-préservent la reconnaissabilité.Comme dans le cas linéaire, nous définissons ensuite la classe des systèmes fortement kbornés FBO(k), qui étend la classe LFBO(k). Nous montrons que le problème de l'appartenance à FBO(k) est décidable. La classe FBO contient strictement la classe des systèmes growing linéaires à gauche. / We introduce k-bounded term rewriting for linear systems (bo(k), for k integer). This strategy is associated with the class of k-bounded systems LBO(k). We show that the systems in the class LBO (union of the LBO(k) for all k), inverse-preserve recognizability. We show that the problems of termination and inverse-termination for the bo(k) strategy are decidable and use this result to show the decidability of these two problems for subclasses of LBO: the classes of linear systems strongly k-bounded: LFBO(k). The class LFBO (union of the LFBO(k)) includes strictly many known classes: the inverse left-basic systems, the linear growing systems, the linear inverse Finite-Path-Overlapping systems. Membership to LFBO(k) is decidable but this is not hte case for LBO(0). For words, we show that the bo(k) strategy preserves algebricity. We extend k-bounded rewriting to left-linear systems. As in the linear case, we associate a class of systems to the strategy: the class of left-linear kbounded systems BO(k) which extends LBO(k). We show that the systems in BO(k) inversepreserve recognizability. As in the linear case, we define the class of strongly k-bounded systems FBO(k), which extends LFBO(k). Membership to FBO(k) is proved decidable. The FBO class contains stricly the class of left-linear growing systems.

Chez Escherichia coli la terminaison de la transcription peut intervenir selon deux mécanismes distincts : tout d'abord la terminaison intrinsèque qui correspond à une séquence ADN, codant pour une structure en tige boucle riche en GC suivie d'une répétition d'uridine sur l'ARN, induisant le relargage de l'ARN polymérase. Le second mécanisme est gouverné par un facteur de terminaison nommé Rho qui gouverne environ 50 % des événements de terminaison chez E. coli. Au cours de ma thèse, je me suis intéressé à ce deuxième mécanisme, et plus particulièrement à sa régulation in vivo (antiterminaison). Rho, sous la forme d'un anneau héxamèrique, se fixe à l'ARN naissant au niveau d'un site d'entrée (également appelé RUT), puis utilise son activité ATPase pour longer l'ARN et dissocier le complexe ternaire d'élongation stoppé au niveau d'un site de pause. Les terminateurs Rho-dépendants sont assez mal définis et peu d'entre eux on été analysés en détail. Le terminateur du tR1 du phage lambda (λ) est le terminateur Rho-dépendant le plus étudié à la fois in vitro et in vivo. La terminaison Rho-dépendante au niveau de ce terminateur est gouvernée principalement par les séquences localisées en 5', codant deux régions du transcript nommées RUTA et RUTB. Ces deux régions sont séparées par le motif ARN BOXB qui n'est pas indispensable à l'action de Rho mais sert, dans le mécanisme d'antiterminaison, de site de fixation pour la protéine N du paghe λ. Grâce à un système minimal d'étude in vivo, nous avons montré que le motif BOXB possède une fonction double dans les mécanismes de terminaiso/antiterminaison au niveau de λtR1 régulant l'expression temporale du génome du phage λ. Sous la forme d'une tige boucle hautement structurée, BOXB agit comme un lien permettant de placer RUTA et RUTB l'un à côté de l'autre pour une interaction optimale avec Rho et une terminaison efficace. A l'inverse, la fixation de la protéine N sur BOXB induit l'antiterminaison au niveau de λtR1 en empêchant l'accès de Rho à l'ARN. Ce double rôle a été démontré in vivo en substituant au couple N/BOXB la « coat protein » du phage MS2 et son motif cible en tige boucle. En complément de ce travail, j'ai utilisé cette faculté d'un complexe ribonucléoprotéïque de bloquer la terminaison Rho-dépendante, pour développer une nouvelle approche d'étude in vivo, des complexe ARN-protéine.

Dans le domaine de l'Optimisation Combinatoire, la résolution de manière optimale de problèmes de grande taille par le biais d'algorithmes Branch-and-Bound requiert un nombre très élevé de ressources de calcul. De nos jours, de telles ressources sont accessibles grâce aux grilles de calcul, composées de grappes de clusters réparties sur différents sites géographiques. Ces environnements parallèles posent de nombreux défis scientifiques, notamment en termes de passage à l'échelle, de la prise en compte de l'hétérogénéité des ressources ainsi qu'en termes de tolérance aux pannes. La plupart des approaches existantes pour l'algorithme Branch-and-Bound parallèle sont basées sur une architecture de type Maître-Esclave, où un processus maître répartit les tâches à accomplir auprès de processus esclaves en charge de les traîter. L'utilisation d'une telle entité centrale constitue un obstacle majeur en ce qui concerne le passage à l'échelle. Dans cette thèse, nous proposons de relever ces défis ainsi que de surmonter cet obstacle grâce à une approche innovante et complètement distribuée, basée sur une architecture Pair-à-Pair (P2P). Celle-ci repose sur un seul type de processus (le pair), qui a pour mission d'explorer son propre ensemble de tâches, de le partager avec d'autres pairs et de diffuser l'information globale. Nous définissons des mécanismes adaptés en lien avec l'algorithme Branch-and-Bound, qui traitent de la répartition de la charge, de la diffusion de la meilleure solution trouvée et de la détection de la terminaison des calculs. En plus de multiples expérimentations sur le problème d'ordonnancement du Flow-Shop sur la grille de calcul Grid'5000, nous proposons une preuve formelle de la correction de notre approche. Par ailleurs, nous traîtons une problématique souvent ignorés dans les travaux relatifs au calcul P2P, qui est l'importance de la topologie du réseau P2P. Généralement, une topologie très simple est utilisée. Les résultats obtenus montrent que notre approche permet le déploiement de réseaux de calculs à de très grandes échelles, constitués potentiellement de centaines de milliers de coeurs de calcul. Notre dernière contribution consiste en une approche Pair-à-Pair tolérante aux pannes afin de prendre en compte la nature généralement très volatile des ressources de calcul. Les résultats obtenus prouvent la robustesse de l'approche dans des environnements à la fois réalistes et sujets à de nombreux dysfinctionnements

Les mitochondries sont des organites présents dans la plupart des cellules eucaryotes et spécialisés dans la production d'énergie, via la chaîne respiratoire localisée dans leur membrane interne. Les mitochondries possèdent leur propre génome et leur propre système d'expression participant à la biogenèse des complexes respiratoires. En particulier la machinerie de traduction mitochondriale, comme les complexes respiratoires, est d'origine génétique double, nucléaire et mitochondriale. De nombreuses maladies humaines résultent de défauts de l'expression des gènes mitochondriaux et en particulier de mutations de facteurs impliqués dans la traduction mitochondriale. La levure Schizosaccharomyces pombe est un modèle de choix pour identifier ces facteurs et comprendre leur fonctionnement car c'est un micro-organisme simple et physiologiquement plus proche des eucaryotes supérieurs que ne l'est Saccharomyces cerevisiae. Lors de ma thèse j'ai tout d'abord participé à la mise en place de nouveaux outils permettant de mieux comprendre le fonctionnement de la traduction mitochondriale, en étiquetant le mitoribosome de S. pombe au niveau de la petite et de la grande sous-unité. Par la suite j'ai mis au point des expériences de fractionnement sur gradient de saccharose pour analyser la sédimentation du ribosome associé ou dissocié et tester si des facteurs donnés sont liés au mitoribosome. Dans un second temps je me suis intéressé à des facteurs qui pouvaient être impliqués dans la terminaison de la traduction. En fait le seul facteur de reconnaissance des codons stop connu chez S. pombe, Mrf1, n'est pas essentiel, et j'ai cherché à comprendre pourquoi. Deux enzymes, des Peptidyl ARNt hydrolase (Pth) nommées Pth3 et Pth4 possédant toutes deux un motif GGQ comme Mrf1, semblaient être de bons candidats pour expliquer que S. pombe puisse se passer de Mrf1. J'ai montré que ces facteurs jouent un rôle dans la biogenèse mitochondriale et plus précisément que Pth4 est à la fois un suppresseur multicopie et un gène létal synthétique de l'absence de Mrf1. Pour finir j'ai travaillé sur une famille de protéines de S. pombe prédites comme impliquées dans le métabolisme des ARN mitochondriaux : les protéines à Pentatrico Peptide Repeat (PPR). Ainsi il existe au moins 9 protéines PPR chez S. pombe nommée de Ppr1 à Ppr8 ainsi que l'ARN polymérase mitochondriale, Rpo41. L'étude de ces protéines PPR a permis de mettre en évidence qu'elles interviennent toutes dans le métabolisme des ARN à différentes étapes, majoritairement stabilité et traduction, et qu'elles ont souvent des cibles spécifiques. Par exemple la protéine Ppr3 est impliquée dans la stabilité du petit ARNr rns alors que Ppr4 est un activateur spécifique de la traduction de cox1 et que Ppr2 est un activateur général de la traduction mitochondriale dont la cible reste à définir. Globalement, ces travaux montrent que S. pombe est un excellent modèle des fonctions mitochondriales, aussi bien pour les études fondamentales que comme outil pour appréhender les organismes plus complexes comme l'homme.

Nous étudions les propriétés, en particulier la terminaison, des systèmes de types dépendants pour le lambda-calcul et la réécriture.

Thèse d'exercice : Médecine. Ophtalmologie : Paris 12 : 2008. / Titre provenant de l'écran-titre. Bibliogr. f. 62-70.

Environ un tiers des maladies humaines, héréditaires ou acquises, sont dues à la génération d’un codon stop prématuré (PTC). Le système de contrôle appelé dégradation des ARNm non-sens (NMD) permet de détecter puis de dégrader des ARNm contenant un PTC. Les facteurs principaux de la NMD : UPF1, UPF2 et UPF3 reconnaissent les PTCs en interagissant avec le complexe de terminaison de traduction contenant les ribosomes, les facteurs de terminaison eRF1, eRF3 et la protéine poly(A) binding (Pab1p en levure). Nous avons pu résoudre la structure d'un tel complexe en levure comprenant un ribosome en cours de traduction en présence d’un ARNt dans le site P et de facteurs de terminaisons dans le site A. Aucune densité n’a pu être observée pour Pab1p indiquant la flexibilité de l’interaction avec ce complexe. Nous avons aussi évalué l’impact des facteurs de la NMD sur la terminaison dans un système de traduction in vitro humain. UPF3B retarde la reconnaissance du codon stop et favorise la dissociation des sous-unités ribosomales. UPF2 abolit l’effet de UPF3B tandis que l’addition de UPF1 n’a pas d’influence dans la terminaison. Par in vivo et in vitro pulldowns, nous avons montré que UPF3B interagit avec eRF3a et UPF1 et pourrait constituer le lien manquant entre la terminaison et la NMD. Nos résultats illustrent la complexité des mécanismes de la terminaison et de la NMD. / Premature termination codons (PTCs) account for approximately one third of inherited and acquired diseases. A surveillance pathway called nonsense-mediated mRNA decay (NMD) detects and degrades PTC-containing transcripts. NMD core factors UPF1, UPF2 and UPF3 mediate the recognition of PTCs by associating with the terminating translation machinery composed of the ribosome, the release factors eRF1 and eRF3 and the poly(A) binding protein (Pab1p in yeast). Using electron cryo-microscopy, we solved such a complex in yeast and observed the translating ribosome, containing a P-site tRNA and an A-site density for the release factors but not for Pab1p indicating that Pab1p is flexibly bound. We also probed the function of NMD factors in mammalian termination using a reconstituted human in vitro translation system. Surprisingly, we found that UPF3B delayed stop codon recognition and promoted ribosomal dissociation. The addition of UPF2 could abolish UPF3B’s effect on translation termination. UPF1 had no influence in the termination process alone or in combination with UPF2. Using in vitro and in vivo pulldowns we found that UPF3B interacts with eRF3a and UPF1, indicating that UPF3B could be the missing link between termination and NMD. Our results point to a complex interplay between the NMD factors and the termination apparatus.

L’architecture et la régulation de la traduction eucaryote fut pendant longtemps un mystère pour les biologistes. Je présente ici un protocole détaillé pour purifier de manière homogène des ribosomes à partir de cellules HeLa, pour des études biochimiques mais également structurales. En utilisant ces ribosomes, j’ai obtenu des cristaux diffractant à faible résolution, pouvant être utilisés pour de futurs travaux. Une analyse par cryo-microscopie électronique (CME) a abouti à une structure à 5 A de résolution, permettant la construction d’un modèle. De plus, les facteurs eRF1 et eRF3 ont permis des premières études de la terminaison de la traduction par CME. Ces protéines en complexe ont également été étudiées par cristallographie aux rayons-X, montrant des interactions jusqu’alors jamais observées. L’ensemble de ce travail fournit des résultats importants pour la préparation et la description de la structure du ribosome humain, pavant la voie vers l’analyse de complexes fonctionnels. / Ribosomes comprise the translational machinery engaged in synthesizing proteins. The architecture and translation regulation of eukaryotic especially, human ribosomes, has been an enigma for a long time. I established a protocol for purifying homogenous ribosomes from HeLa cells which can be used for structural as well as biochemical analysis. Using these ribosomes, I obtained plate-like crystals of 80S diffracting to low resolution. A cryo electron microscopy analysis of these ribosomes yielded 5 Å resolution structure with secondary structures of rRNA and protein clearly visible. Furthermore, these ribosomes, along with the eukaryotic release factors (eRF1 and eRF3) purified by over-expression in bacteria, formed the basis for translation termination studies using cryo electron microscopy. Simultaneously, eRF1-eRF3 protein complex was explored by X-ray crystallography revealing new interactions. Together, this work paves the way for the analysis of functional ribosome complexes.

La transcription bactérienne est un processus dans lequel l'information codée dans l'ADN est transféré à l'ARN messager (ARNm). Au cours de la dernière étape de ce procédé, la terminaison de la transcription, l'ARNm est libéré et peut être utilisé pour la synthèse des protéines. Un type de terminaison de la transcription décrit chez les bactéries est la terminaison Rho-dépendante. Le rôle de Rho a été largement étudié dans le modèle à Gram négatif bactérie, Escherichia coli dans laquelle Rho est une protéine essentiel est abondant. En revanche, la connaissance de Rho chez les bactéries qui il ne sont pas essentiels et est présent en faibles quantités: par exemple Gram-positif Bacillus subtilis reste limité..Pour étudier le rôle de Rho dans le contrôle de l'expression des gènes chez B. subtilis plusieurs analyses à grande échelle ont été réalisées, y compris des tests d'interactions physiques et fonctionnelles et une analyse globale des changements observés dans l'expression des gènes en corrélation avec la production de protéines.En effet, un ensemble des Rho-spécifiques interactions physiques et fonctionnelles ont été établies. En outre, de nouveaux phénotypes de mutant dépourvu de rho ont été décrits ce qui élucider le rôle de Rho dans le contrôle des différents aspects de la physiologie cellulaire. / Bacterial transcription is a process in which the information encoded in DNA is transferred to messenger RNA (mRNA). During the final step of this process, transcription termination, mRNA is released and can be used for protein synthesis. One type of transcription termination described in bacteria is Rho-dependent termination. The role of Rho has been widely investigated in model Gram-negative bacterium, Escherichia coli in which Rho is essential an abundant protein. In contrast, the knowledge about Rho inbacteria in which it is not essential and is present in low amounts, i. e. Gram-positive Bacillus subtilis remains limited.To investigate the role of Rho in control of gene expression in B. subtilis several large-scale analysis were performed. In effect, a set of Rho-specific physical and functional interactions were established. Additionally, new phenotypes of rho-null mutant were described unraveling the role of Rho in control of different aspects of cell physiology.