L'objectif de cette thèse est d'explorer des descriptions formelles pour la structure et le fonctionnement des systèmes biologiques, ainsi que des outils formels pour raisonner au sujet de leur comportement. Cette thèse s'inscrit dans les travaux étudiant les modèles informatiques sûrs où les calculs sont exprimés par l'intermédiaire de la réécriture, et où nous pouvons compter sur la vérification formelle pour exprimer et valider les propriétés des modèles. Dans cette thèse nous développons un calcul de réécriture d'ordre supérieur pour décrire des molécules, des règles de réaction, et la génération des réseaux biochimiques. Le calcul est basé sur la métaphore chimique en décrivant les calculs en termes de solutions chimiques dans lesquelles les molécules représentant des données agissent l'une sur l'autre librement selon des règles de réaction. Ainsi nous avons obtenu un Calcul Biochimique Abstrait étendant le modèle chimique d'ordre supérieur en considérant des molécules structurées. Le calcul est équipé d'une spécification naturelle de la concurrence et des mécanismes de contrôle grâce à l'expression des stratégies de réécriture sous forme de molécules. La description des complexes moléculaires ou des réactifs chimiques appartient à une classe spécifique de graphes. Nous définissons la structure des graphes avec ports et nous montrons que les principes du calcul biochimique instanciés pour les graphes avec ports sont assez expressifs pour modéliser des systèmes autonomes et des réseaux biochimiques. En plus, les techniques de la réécriture stratégique ouvrent la voie au raisonnement basé sur les calculs et à la vérification des propriétés des systèmes modélisés.

Pour modéliser le fonctionnement d'un système, décrire une situation ou représenter des idées, on se met intuitivement à dessiner des bulles et les lier par des flèches sous forme de graphes étiquetés. Les logiques modales constituent un cadre formel expressif et extensible qui permet de définir ces graphes sous forme de « modèles », et d'exprimer certaines propriétés de ces graphes sous forme de « formules » afin de pouvoir raisonner là-dessus: model checking, test de satisfiabilité ou de validité, etc. Pour des formules et modèles de tailles importantes, ces tâches deviennent compliquées. De ce fait, un outil permettant de les réaliser automatiquement s'avère nécessaire. LoTREC en est un exemple. Il permet à son utilisateur de créer sa propre méthode de preuve, grâce à un langage simple et de haut niveau, sans avoir besoin d'aucune expertise spécifique en programmation. Durant ma thèse, j'ai revu le travail qui était déjà accompli dans LoTREC et j'ai apporté de nouvelles extensions qui s'avéraient nécessaires pour pouvoir traiter de nouvelles logiques (K.alt1, universal modality, Hybrid Logic HL(@),Intuitionistic logic, Public Announcement Logic, ...) et offrir à l'utilisateur certaines nouvelles techniques. D'autre part, j'ai examiné les origines de LoTREC dans le monde de réécriture de graphes et j'ai spécifié la sémantique de son moteur de réécriture. Cela a permis d'éclaircir comment l'on peut hériter dans nos méthodes de preuve des résultats et des propriétés théoriques déjà bien établies dans le domaine de la réécriture de graphes.

Ces dernières années, on a assisté au développement du<br />calcul de réécriture, encore appelé rho-calcul, qui intègre de<br />façon uniforme la réécriture de premier ordre et le lambda-calcul.<br />Cette thèse est dédiée à l'étude des capacités d'expression du calcul de réécriture, avec un intérêt particulier pour la réécriture d'ordre supérieur et la possibilité de manipuler des graphes.<br /><br />Dans la première partie de cette thèse, la relation entre le calcul de réécriture et la réécriture d'ordre supérieur, en particulier les Combinatory Reduction Systems (CRSs), est étudiée.<br />Nous présentons d'abord un algorithme de filtrage original<br />pour les CRSs qui utilise une traduction des termes CRS en<br />lambda-termes et le filtrage d'ordre supérieur classique du lambda-calcul. Nous proposons ensuite un encodage des CRSs dans le rho-calcul<br />basé sur la traduction de chaque réduction CRS<br />en une réduction correspondante dans le rho-calcul.<br />Dans la deuxième partie, nous présentons une extension du rho-calcul,<br />appelé calcul de réécriture de graphes (ou Rg-calcul),<br />qui gère des termes avec partage et cycles.<br />Le calcul sur les termes est généralisé de manière naturelle en utilisant des contraintes d'unification en plus des contraintes de filtrage standard du rho-calcul.<br /><br />Le Rg-calcul est alors montré confluent sur des classes<br />d'équivalence de termes, sous certaines restrictions de linéarité sur les motifs, et assez<br />expressif pour simuler la réécriture de termes graphes et le<br />lambda-calcul cyclique.

Dans cette thèse, nous présentons à la fois une collection de modèles de générations de réseaux et de diffusion d'information exprimés à l'aide d'un formalisme particulier appelé la réécriture de graphes, ainsi qu'une nouvelle méthode de représentation permettant la visualisation de la diffusion d'information dans des grands réseaux sociaux. Les graphes sont des objets mathématiques particulièrement versatiles qui peuvent être utilisés pour représenter une large variété de systèmes abstraits. Ces derniers peuvent être transformés de multiples façons (création, fusion ou altération de leur éléments), mais de telles modifications doivent être contrôlées afin d'éviter toute opération non souhaitée. Pour cela, nous faisons appel au formalisme particulier de la réécriture de graphes afin d'encadrer et de contrôler toutes les transformations. Dans notre travail, un système de réécriture de graphes opère sur un graphe, qui peut être transformé suivant un ensemble de règles, le tout piloté par une stratégie. Nous commençons tout d'abord par utiliser la réécriture en adaptant deux algorithmes de génération de réseaux, ces derniers permettant la création de réseaux aux caractéristiques petit monde. Nous traduisons ensuite vers le formalisme de réécriture différents modèles de diffusion d'information dans les réseaux sociaux. En énonçant à l'aide d'un formalisme commun différents algorithmes, nous pouvons plus facilement les comparer, ou ajuster leurs paramètres. Finalement, nous concluons par la présentation d'un nouvel algorithme de dessin compact de grands réseaux sociaux pour illustrer nos méthodes de propagation d'information. / In this thesis, we present a collection of network generation and information diffusion models expressed using a specific formalism called strategic located graph rewriting, as well as a novel network layout algorithm to show the result of information diffusion in large social networks. Graphs are extremely versatile mathematical objects which can be used to represent a wide variety of high-level systems. They can be transformed in multiple ways (e.g., creating new elements, merging or altering existing ones), but such modifications must be controlled to avoid unwanted operations. To ensure this point, we use a specific formalism called strategic graph rewriting. In this work, a graph rewriting system operates on a single graph, which can then be transformed according to some transformation rules and a strategy to steer the transformation process. First, we adapt two social network generation algorithms in order to create new networks presenting small-world characteristics. Then, we translate different diffusion models to simulate information diffusion phenomena. By adapting the different models into a common formalism, we make their comparison much easier along with the adjustment of their parameters. Finally, we finish by presenting a novel compact layout method to display overviews of the results of our information diffusion method.

L'objectif de cette thèse est d'explorer des descriptions formelles pour la structure et le fonctionnement des systèmes biologiques, ainsi que des outils formels pour raisonner au sujet de leur comportement. Cette thèse s'inscrit dans les travaux étudiant les modèles informatiques sûrs où les calculs sont exprimés par l'intermédiaire de la réécriture, et où nous pouvons compter sur la vérification formelle pour exprimer et valider les propriétés des modèles. Dans cette thèse nous développons un calcul de réécriture d'ordre supérieur pour décrire des molécules, des règles de réaction, et la génération des réseaux biochimiques. Le calcul est basé sur la métaphore chimique en décrivant les calculs en termes de solutions chimiques dans lesquelles les molécules représentant des données agissent l'une sur l'autre librement selon des règles de réaction. Ainsi nous avons obtenu un Calcul Biochimique Abstrait étendant le modèle chimique d'ordre supérieur en considérant des molécules structurées. Le calcul est équipé d'une spécification naturelle de la concurrence et des mécanismes de contrôle grâce à l'expression des stratégies de réécriture sous forme de molécules. La description des complexes moléculaires ou des réactifs chimiques appartient à une classe spécifique de graphes. Nous définissons la structure des graphes avec ports et nous montrons que les principes du calcul biochimique instanciés pour les graphes avec ports sont assez expressifs pour modéliser des systèmes autonomes et des réseaux biochimiques. En plus, les techniques de la réécriture stratégique ouvrent la voie au raisonnement basé sur les calculs et à la vérification des propriétés des systèmes modélisés / The objective of this thesis is to explore formal descriptions for the structure and functioning of biological systems, as well as formal tools for reasoning about their behavior. This work takes place in the overall prospective to study safe computational models where computations are expressed via rewriting, and where we can rely on formal verification to express and validate suitable properties. In this thesis we develop a higher-order calculus rewriting for describing molecules, reaction patterns, and biochemical network generation. The calculus is based on the chemical metaphor by describing the computations in terms of chemical solutions in which molecules representing data freely interact according to reaction rules. This way we obtained an Abstract Biochemical Calculus as an extension of the higher-order chemical model by considering structured molecules. The calculus is provided with a natural specification of concurrency and of controlling mechanisms by expressing rewrite strategies as molecules. The description of molecular complexes or chemical reactants belong to specific classes of graphs. We define the structure of port graphs and we show how the principles of the biochemical calculus instantiated for port graphs are expressive enough for modeling autonomous systems and biochemical networks. In addition, strategic rewriting techniques open the way to reason about the computations and to verify properties of the modeled systems

Les travaux de cette thèse portent sur l'analyse syntaxique et sémantique de la phrase, en utilisant pour l'analyse syntaxique un formalisme grammatical lexicalisé polarisé et en prenant comme exemple les grammaires d'interaction. Dans les formalismes grammaticaux lexicalisés, les polarités permettent de contrôler explicitement la composition des structures syntaxiques. Nous exploitons d'abord le besoin de composition exprimé par certaines polarités pour définir une notion faible de réduction de grammaire applicable à toute grammaire lexicalisée polarisée. Nous étudions ensuite la première phase de l'analyse syntaxique des formalismes lexicalisés: l'étiquetage grammatical. Nous exploitons là encore le besoin de composition de certaines polarités pour concevoir trois méthodes symboliques de filtrage des étiquetages grammaticaux que nous implantons sur automate. Nous abordons enfin l'interface syntaxe-sémantique des formalismes lexicalisés. Nous montrons comment l'utilisation de la réécriture de graphes comme modèle de calcul permet concrètement d'utiliser des structures syntaxiques riches pour calculer des représentations sémantiques sous-spécifiées.

Comme dans de nombreux autres domaines, la construction des applications en Informatique Ambiantes (IAm) se fait par réutilisation d'entités logicielles disponibles. Pour des raisons de conductivités, de pannes, de charge de batterie mais aussi de nombreuses autres, la disponibilité de ces entités est imprévisible ce qui implique que l'auto-adaptation dynamique des applications est une nécessité. Cela passe par la spécification en parallèle des adaptations par des experts de divers domaines. Ce parallélisme de construction, peut amener des problèmes d'interférences lors de la composition dynamique de plusieurs adaptations. Dans cette thèse, par l'utilisation de graphes, nous contribuons à la définition d'un cadre formel pour la détection et la résolution de ces interférences. L'assemblage des entités logicielles repose sur des connecteurs d'assemblage qui sont utilisés dans la spécification des adaptations. Des règles de réécriture de graphe permettront de résoudre les interférences détectées, cette résolution étant guidée par la connaissance de connecteurs définis. De plus, pour pouvoir étendre dynamiquement et automatiquement notre mécanisme de gestion des interférences, nous proposons la modélisation comportementale de ces connecteurs. Ceci permet de ne pas reposer sur une connaissance à priori des connecteurs et autorise par la même d'étendre dynamiquement l'ensemble des connecteurs disponibles pour la spécification des adaptations.

Comme dans de nombreux autres domaines, la construction des applications en Informatique Ambiantes (IAm) se fait par réutilisation d’entités logicielles disponibles. Pour des raisons de conductivités, de pannes, de charge de batterie mais aussi de nombreuses autres, la disponibilité de ces entités est imprévisible ce qui implique que l’auto-adaptation dynamique des applications est une nécessité. Cela passe par la spécification en parallèle des adaptations par des experts de divers domaines. Ce parallélisme de construction, peut amener des problèmes d’interférences lors de la composition dynamique de plusieurs adaptations. Dans cette thèse, par l’utilisation de graphes, nous contribuons à la définition d’un cadre formel pour la détection et la résolution de ces interférences. L’assemblage des entités logicielles repose sur des connecteurs d’assemblage qui sont utilisés dans la spécification des adaptations. Des règles de réécriture de graphe permettront de résoudre les interférences détectées, cette résolution étant guidée par la connaissance de connecteurs définis. De plus, pour pouvoir étendre dynamiquement et automatiquement notre mécanisme de gestion des interférences, nous proposons la modélisation comportementale de ces connecteurs. Ceci permet de ne pas reposer sur une connaissance à priori des connecteurs et autorise par la même d’étendre dynamiquement l’ensemble des connecteurs disponibles pour la spécification des adaptations. / Like many other fields, application construction in ubiquitous computing is done by reuse of available software entities. For reasons of conductivity, breakdown, battery charge, but also many others reasons, the availability of these entities is unpredictable. As consequence, the self-adaptation of applications becomes necessary. This requires the specification of parallel adaptations by experts from various fields. This parallel specification can cause interference problems when several adaptations are composed. In this thesis, using graph formalism, we contribute to the definition of a formal approach for the detection and the resolution of interferences. The specification of adaptation uses connectors in order to assemble software entities. Graph rewriting rules are defined to solve the detected interferences. This resolution is guided by the knowledge of defined connectors. In addition, in order to extend dynamically and automatically our interference management mechanism, we propose behavioral modeling of these connectors. This allows us extending our mechanism without an a priori knowledge of connectors and allows afterwards to extend the set of available connectors used for adaptations' specifications.

Étant une représentation formelle et explicite des connaissances d'un domaine, les ontologies font régulièrement l'objet de nombreux changements et ont ainsi besoin d'être constamment adaptées pour notamment pouvoir être réutilisées et répondre aux nouveaux besoins. Leur réutilisation peut prendre différentes formes (évolution, alignement, fusion, etc.), et présente plusieurs verrous scientifiques. L'un des plus importants est la préservation de la consistance de l'ontologie lors de son changement. Afin d'y répondre, nous nous intéressons dans cette thèse à étudier les changements ontologiques et proposons un cadre formel capable de faire évoluer et de fusionner des ontologies sans affecter leur consistance. Premièrement, nous proposons TGGOnto (Typed Graph Grammars for Ontologies), un nouveau formalisme permettant la représentation des ontologies et leurs changements par les grammaires de graphes typés. Un couplage entre ces deux formalismes est défini afin de profiter des concepts des grammaires de graphes, notamment les NAC (Negative Application Conditions), pour la préservation de la consistance de l'ontologie adaptée.Deuxièmement, nous proposons EvOGG (Evolving Ontologies with Graph Grammars), une approche d'évolution d'ontologies qui se base sur le formalisme GGTOnto et traite les inconsistances d'une manière a priori. Nous nous intéressons aux ontologies OWL et nous traitons à la fois : (1) l'enrichissement d'ontologies en étudiant leur niveau structurel et (2) le peuplement d'ontologies en étudiant les changements qui affectent les individus et leurs assertions. L'approche EvOGG définit des changements ontologiques de différents types (élémentaires, composées et complexes) et assure leur implémentation par l'approche algébrique de transformation de graphes, SPO (Simple PushOut). Troisièmement, nous proposons GROM (Graph Rewriting for Ontology Merging), une approche de fusion d'ontologies capable d'éviter les redondances de données et de diminuer les conflits dans le résultat de fusion. L'approche proposée se décompose en trois étapes : (1) la recherche de similarité entre concepts en se basant sur des techniques syntaxiques, structurelles et sémantiques ; (2) la fusion d'ontologies par l'approche algébrique SPO ; (3) l'adaptation de l'ontologie globale résultante par le biais des règles de réécriture de graphes.Afin de valider les travaux menés dans cette thèse, nous avons développé plusieurs outils open source basés sur l'outil AGG (Attributed Graph Grammar). Ces outils ont été appliqués sur un ensemble d'ontologies, essentiellement sur celles développées dans le cadre du projet européen CCAlps (Creatives Companies in Alpine Space) qui a financé les travaux de cette thèse. / Ontologies are a formal and explicit knowledge representation. They represent a given domain by their concepts and axioms while creating a consensus between a user community. To satisfy the new requirements of the represented domain, ontologies have to be regularly updated and adapted to maintain their consistency. The adaptation may take different forms (evolution, alignment, merging, etc.), and represents several scientific challenges. One of the most important is to preserve the consistency of the ontology during the changes. To address this issue, we are interested in this thesis to study the ontology changes and we propose a formal framework that can evolve and merge ontologies without affecting their consistency.First we propose TGGOnto (Typed Graph Grammars for Ontologies), a new formalism for the representation of ontologies and their changes using typed graph grammars (TGG). A coupling between ontologies and TGG is defined in order to take advantage of the graph grammars concepts, such as the NAC (Negative Application Conditions), in preserving the adapted ontology consistency. Second, we propose EvOGG (Evolving Ontologies with Graph Grammars), an ontology evolution approach that is based on the TGGOnto formalism that avoids inconsistencies using an a priori approach. We focus on OWL ontologies and we address both : (1) ontology enrichment by studying their structural level and (2) ontology population by studying the changes affecting individuals and their assertions. EvOGG approach defines different types of ontology changes (elementary, composite and complex) and ensures their implementation by the algebraic approach of graph transformation, SPO (Single pushout).Third, we propose GROM (Graph Rewriting for Ontology Merging), an ontologies merging approach that avoids data redundancy and reduces conflict in the merged result. The proposed approach consists of three steps: (1) the similarity search between concepts based on syntactic, structural and semantic techniques; (2) the ontologies merging by the algebraic approach SPO; (3) the global ontology adaptation with graph rewriting rules.To validate our proposals, we have developed several open source tools based on AGG (Attributed Graph Grammar) tool. These tools were applied to a set of ontologies, mainly on those developed in the frame of the CCAlps (Creatives Companies in Alpine Space) European project, which funded this thesis work.

Ce travail est une étude approfondie de la concurrence dans les extensions non-déterministes des réseaux d'interaction de Lafont (langage graphique qui représente, lui, le calcul fonctionnel). Ces extensions sont de trois sortes : les réseaux multirègles, multiports et multifils, et leurs combinaisons donnent ainsi sept types de réseaux. Un premier travail consiste à déterminer une bonne sémantique pour pouvoir comparer ces extensions. On cherche à définir un sémantique opérationnelle structurelle sur les réseaux en se basant sur des technique connues de réécriture des graphes, plus particulièrement celle de " double-pushout with borrowed contexts ". Nous définissons à partir de cette méthode un système d'étiquetage des transitions donné par des règles de dérivations dans le style des langages de processus qui sont le paradigme principal pour étudier les systèmes de calcul concurrents. Nous définissons de plus une sémantique observationnelle sur les réseaux basée sur une notion paramétrique de barbe, qui permet enfin de donner avec précision une notion de traduction entre systèmes. On considère qu'une extension est plus expressive qu'une autre si tout langage de la seconde peut être traduit dans un langage de la première. Ceci nous permet de classer l'ensemble des extensions de manière hiérarchique en trois groupe selon la possibilité de traduire un système de réseau dans un autre. Du plus fort au plus faible : les réseaux contenant des multiports ; ensuite ceux contenant des multifils; enfin les réseaux multirègles. Ceci nous permet de donner un langage universel pour les réseaux dont l'étude donne un point de vue neuf sur les briques fondamentales de la concurrence.