Un automate temporisé est un automate augmenté avec plusieurs horloges qui mesurent le passage de temps et peuvent conditionner la modification de l'état du système. Les automates temporisés ont été introduits en tant que modèle formel pour les systèmes temps-réel, en espérant que leur rôle dans la vérification de tels systèmes sera similaire au rôle des automates finis dans la recherche systématique des erreurs de conception de systèmes non-temporisés. Dans notre thèse nous étudions plusieurs questions théoriques liés aux automates temporisés et aux langages temporisés. Dans une première partie nous étudions une sous-classe simple d'automates temporisés à une seule horloge qui est remise à zéro pendant chaque transition. Nous montrons que cette sous-classe supporte des résultats similaires à la théorie classique des automates finis: des théorèmes de Kleene, de Myhill-Nerode et de fermeture par complémentation. La deuxième et principale partie de la thèse est motivée par les expressions régulières temporisés de Asarin, Caspi et Maler. Depuis leur introduction, on sait qu'il faut employer l'intersection dans les expressions régulières pour que leur expressivité soit égale aux automates temporisés. Nous poursuivons alors une approche alternative en utilisant des parenthèses colorées pour définir les contraintes temporelles sur une séquence d'événements. Cette idée aboutit à une représentation alternative des langage des automates temporisés, basée sur une nouvelle classe de langages formels que nous appelons . Nous développons alors la théorie des expressions régulières sur les regminos et nous montrons que le problème de sémantique vide est indécidable en cas général, et décidable pour une sous-classe large de langages. L'application de ces résultats nous amène à des nouvelles structures de données et à des algorithmes pour le problème du langage vide dans les automates temporisés et les expressions régulières.

Dans cette thèse, nous présentons une quantification de la déformation en cours du sud des Balkans et de la Méditerrnée centrale et orientale par GPS. Le champs de vitesses a été déduit de l'analyse de données issues de 225 stations GPS permanentes ou épisodiques pour la période 1996-2009. Ce champs de vitesse est analysé et discuté pour essayer de déterminer si le champ de vitesse est continu ou si, au contraire, des blocs stables peuvent être individualisés. La déformation actuelle du sud-ouest de la Bulgarie et du nord de la Grèce ont été particulièrement étudiés à partir de mesures réalisées de 1996 à 2008. Cette région est particulièrement active comme le montre la sismicité historique et en particulier le séisme de Krupnik en 1904 (sud-ouest de la Bulgarie) qui fut un séisme parmi les plus destructeur en Europe continentale au cours des deux derniers siècles. Le nord de la Grèce est quant à lui caractérisé par des séismes destructeurs de M > 6. Les résultats obtenus montrent l'existence de déplacements vers le sud par rapport à l'Eurasie stable s'accroissant du Nord (2mm/an) vers le sud de la région étudiée (10 mm/an). Les tenseurs de taux de déformation sont présentés et discutés à la lumière de la déformation exprimée lors des séismes. Ces deux types d'information montrent tous deux une prédominance d'une extension Nord-sud en accord avec les données géologiques (présence de grabens Est-Ouest) et les modèle proposés pour la Méditerranée centrale et orientale. A l'ouest des Balkans, la déformation actuelle de l'Albanie s'exprime par des nombreux indices néotectoniques et une sismicité importante présentant de nombreux séismes historiques destructeurs. Données géologiques et sismotectoniques montrent d'une part l'existence d'un raccourcissement dans les Albanides externes et d'autre part une extension Est-Ouest et Nord -Sud dans les Albanides externes. Les vitesses de déplacements ont été quantifiées par GPS continu et épisodiques à partir de 2003. Ces vitesses ainsi que les mécanismes au foyer montrent un raccourcissement en cours à travers l'Adriatique (déplacements des Albanides externes vers l'ouest par rapport à la plaque Apulie), et un déplacement vers le sud des Albanides internes à la fois par rapport à la plaque Apulie et à la plaque Eurasie. La zone de failles Skutar-Pesh entre Albanides et Dinarides semble former la limite nord de la zone affectée par un déplacement vers le sud par rapport à l'Eurasie comprenant l'est de l'Albanie, la Macédoine, la Bulgarie et la Grèce. Les Albanides externes semblent être segmentées par des failles transverses actives (faille de Lezhë et de l'ile d'Othoni et du col de Dhërmi) associées à une importante sismicité historiques. Les Albanides internes sont affectées à la fois par une extension Nord-sud le long de la faille d'Elbasani-Diber, du graben de Korca et par une extension est-ouest de part et d'autre du graben d'Ohrid. Le domaine affecté par un déplacement vers le sud est donc limité à l'ouest par la transition antre les Albanides externes et les Albanides Internes et au nordouest par la faille de Skutar-Pesh qui se poursuit en Macédoine. Sur l'ensemble du domaine étudié, notre analyse du champ de vitesse nous conduit à privilégié l'hypothèse d'une déformation continue au détriment d'une déformation localisée aux frontières de blocs stables.

Ces derniers temps, de nouvelles données riches en information ont été produites : les Séries Temporelles d'Images Satellitaires qui permettent d'observer les évolutions de la surface de la Terre. Ces séries constituent un grand volume de données et elles contiennent des informations complexes et d'intérêt. Par exemple, de nombreux événements spatio-temporels, tels que les récoltes, la maturation de cultures ou l'évolution de zones urbaines, peuvent y être obsérvés et sont utiles pour des problèmatiques de télé-surveillance. Dans ce contexte, cette thèse se propose d'extraire l'information automatiquement pour aider à la compréhension des événements spatio-temporels et de compresser pour limiter l'espace de stockage. Aussi l'objectif majeur de ces travaux consiste en la conception d'une méthodologie incorporant conjointement l'extraction d'information et la compression. Ce traitement conjoint nous permet d'obtenir une représentation compacte des Séries Temporelles d'Images Satellitaires qui contienne un index du contenu informationnel. Plus précisément, ces travaux décrivent dans un premier temps le concept d'extraction et de compression conjointes où l'extraction est vue comme une compression avec pertes de l'information. Dans un second temps, deux méthodologies élaborées à partir du concept précédent sont présentées. La première permet de construire un index du contenu informationnel en se fondant sur le principe d'Information Bottleneck. La seconde permet de construire un code ou une représentation compacte qui intègre un index du contenu informationnel. Finalement, ces deux méthodes sont validées et comparées sur des données synthétiques et sont par la suite appliquées avec succès aux Séries Temporelles d'Images Satellitaires.

Cette thèse présente Adetoa, système dédié au repérage et à l'annotation sémantique automatique d'expressions temporelles dans des pages Web pour une application de e-tourisme. Une étude linguistique détaillée a permis de mettre en avant les caractéristiques et la complexité de l'expression de la temporalité dans les pages Web touristiques. Une étude sémiotique de ce type de pages a montré que les données y étaient organisées de manière fort variée, ne présentant aucune régularité, ce qui rend difficile voire parfois impossible l'automatisation de leur analyse. Ces analyses ont mené à l'élaboration d'un ensemble important de transducteurs (avec Unitex) pour les tâches de repérage et d'annotation des expressions temporelles, ce qui constitue une ressource pouvant être généralisée. De plus, d'autres informations du domaine touristique sont repérées : les objets du tourisme et les adresses. Des transducteurs de liage permettent de grouper toutes les informations concernant une même offre touristique. Pour l'annotation et l'intégration d'Adetoa à la chaîne de traitement du projet Eiffel, un schéma d'annotation et des règles de transformations ont été mis au point. Sans en être un calque direct, le schéma d'annotation suit une ontologie du tourisme. Il permet ainsi de rester au plus près des expressions linguistiques de manière à les caractériser finement. L'ontologie a ensuite pu être adaptée en conséquence, pour un meilleur stockage des données dans la base de connaissance qui lui correspond. L'évaluation d'Adetoa, présentée dans cette thèse, a montré des résultats satisfaisants aussi bien d'un point de vue théorique que pour cette application industrielle.

Alors que la composition de musique électro-acoustique mobilise de plus en plus d'outils numériques, la question de l'interprétation de telles pièces reste ouverte. La plus part du temps, ces pièces sont un enregistrement sur support, d'une organisation temporel d'un matériau sonore. Pendant l'exécution, l'oeuvre est simplement diffusée et l'interprète peut uniquement modifier des paramètres globaux tels que le volume, la balance ou la spatialisation sur le système d'écoute. Il ne peut pas interpréter la pièce au sens où il pourrait le faire pour une partition classique. Nous souhaiterions que ce type d'interprétation soit possible pour les pièces électro-acoustiques. Cette possibilité ne peut être posible que dans le cadre de ``partitions interactives'' capables de s'adapter à leur environnement (contrôles de l'interprète, autres musiciens). Dans ce contexte, la partition est exécutée par la machine, ce qui conduit à s'intéresser à un problème différent de celui du suivi de partition. Nous cherchons à élaborer un système constitué de deux parties : un environnement de composition assistée par ordinateur permettant au compositeur de créer de telles partitions interactives, et une machine d'exécution rendant possible leur interprétation. L'environnement de composition doit disposer d'une représentation formelle de la musique ``interprétable''. Nous nous appuyons donc sur une formalisation de l'interprétation de la musique instrumentale, et cherchons alors à la généraliser à des pièces impliquant des processus génériques à la place des notes. Nous focalisons notre étude sur un certain aspet de l'interprétation : les variations agogiques, c'est à dire la possibilité pour l'interprète de modifier les date d'occurrence d'événements discrets de la pièces pendant l'exécution. Ces modifications de dates sont accessibles grace à des ``point d'interactions'' (débuts, fins, ou points intermédiaires) des processus, dont la position temporelle permet de contrôler la temporalité de la pièce. Mais ces possibilités sont encadrées par le compositeur à la création de la partition (comme dans le cas de musique instrumentale). Ces contraintes sont le résultats d'une démarche de composition, elles permettent également d'éviter une désorganisation totale de la pièce pendant l'exécution. Nous proposons une représentation formelle des partitions interactives, basées sur des blocs 2D, telle celle des Maquettes d'OpenMusic ou des Data Structures de Pure Data. Les partitions sont des ensembles d'objets organisés sur une ligne de temps ; ces objets sont eux-mêmes représentés comme des séquences de points de contrôle discrets (début, fin et points intermédiares). Ils représentent l'exécution de processus responsables du rendu sonore de la pièce (synthèse et traintement de signal ou de symboles ou même opérations algorithmiques complexes). Pour définir les limites imposées à l'interprétation, le compositeur peut poser des contraintes temporelles entre les points de contrôle de la pièce ; il peut ainsi imposer un ordre partiel entre les événements à l'aide de contraintes qualitatives, ou utiliser des contraintes quantitatives pour limiter les valeurs possibles des intervalles de temps séparant les points de contrôle. La partition est alors à la fois complètement spécifiée, mais sa temporalité reste flexible, laissant ainsi la place à l'interprétation. De plus, le compositeur peut définir certains points de contrôle comme ``interactifs'', les rendre ainsi dynamiquement déclenchables à l'arrivée d'événements extérieurs, supposés se produire pendant l'exécution de la pièce. Ces événements peuvent être produits par des interfaces de contrôle, ou par la détection de situations particulières dans le contexte musical. Lorsqu'une partition est interprétée, la machine d'exécution envoie un message aux processus lorsqu'un point de contrôle doit se produire. Ceci peut être le fait de l'écoulement du temps pour les points non dynamiques, ou de l'arrivée de événement extérieur correspondant pour les points dynamiques. Le système s'assure que les contraintes temporelles définies par le compositeur ne sont pas violées. Si l'arrivée d'un événement extérieur remet en cause la validité de contraintes, le système recalcule les dates de points de contrôle futurs pour assurer la validité des contraintes. L'ordre entre les points peut alors être modifié. Ces calculs sont effectués par un algorithme de propagation de contraintes. Le maintien des contraintes temporelles, peut amener le système à ignorer des événements extérieurs lorsque ceci risque de contredire des contraintes, tout comme il devra simuler l'arrivée d'un événement dans cas où l'absence de ce dernier conduirait à violer une contrainte. Nous proposons une struture de machine abstraite capable d'exécuter dynamiquemenr les partitions interactives. Celle-ci est basée sur les réseaux de Petri et la propagation de contraintes. Nous donnons un algorithme pour compiler les partitions depuis leur descritption formelle vers une représentation exécutable par la machine. Nous avons également développé un prototype dans OpenMusic, sous la forme d'une extension des Maquettes pour l'édition des partitions utilisant un système de propagation de contraintes. Elle contient également un compilateur de partition et une machine d'exécution envoyant des messages UDP vers des applications tierces. Les partitions sont sauvergardées grace à un format XML d'échange. Nous présentons plusieurs applications du système à la musique électro-acoustique la musique instrumentale et le théâtre.

Cette thèse s'organise autour du but suivant : comment trouver un bon modèle pour les séries temporelles qui subissent des changements de comportement? L'application qui a motivé cette question est la caractérisation des crises financières à l'aide d'un indice des chocs de marché inspiré de la géophysique et de modèles hybrides à changements de régime intégrant des perceptrons multi-couches. Les résultats obtenus sur les données fournissent une séparation intéressante entre deux états relatifsà deux comportements différents du marché, mais des questions sur la sélection de modèles et le choix du nombre de régimes se posent alors naturellement.<br />On propose d'étudier ces questions à travers deux approches. Dans la première, il s'agit de montrer la consistance faible d'un estimateur de maximum de vraisemblance pénalisée sous des conditions de stationnarité et dépendance faible. Les hypothèses introduites sur l'entropie à crochets de la classe des fonctions scores généralisés sont ensuite vérifiées dans un cadre linéaire et gaussien. La deuxième approche, plutôt empirique, est issue des méthodes de classification non-supervisée et combine les cartes de Kohonen avec une classification hiérarchique pour laquelle une nouvelle dispersion basée sur la somme des carrés résiduelle est introduite.

Nous analysons les séries temporelles des glissements de terrain de Nouvelle-Zélande (NZ) en temps et en taux et mettons en évidence une corrélation dans les occurrences de glissements. Cette corrélation n'est pas due aux interactions glissement-séisme ou glissement-glissement mais aux interactions glissement-climat. Nous comparons la dynamique des glissements en temps, espace et taux pour la NZ, le Yosemite (Californie, Etats-Unis), Grenoble (Isère), Val d'Arly (Haute-Savoie), l'Australie et le Wollongong (New South Wales, Australie). Les taux journaliers de glissements de la NZ, du Yosemite, de l'Australie et du Wollongong acceptent une loi puissance pour des taux variant de 1 à 1000 glissements/jour. Cela suggère que les mêmes méchanismes sont à l'oeuvre pour le déclenchement de plusieurs centaines de glissements comme de un seul glissement. L'analyse jointe de ces six catalogues nous a permis de dériver des paramètres permettant de classer la dynamique de chaque endroit en terme de glissements. Enfin, nous comparons les distributions en espace des répliques sismiques et des glissements de terrain déclenchés par les séismes de Chi-Chi (Mw7.6 - Taiwan), du Kashmir (Mw7.6 - Pakistan), de Fiordland (Mw7.2 - NZ), de Northridge (Mw6.6 - Californie) et de Rotoehu (MW5.6 - NZ). Les répliques sismiques et les glissements présentent des distributions spatiales similaires. Nous ne trouvons pas de réponse linéaire entre les glissements et/ou les répliques et les observations de mouvements du sol. Nous suggérons que les glissements et les répliques sont contrôlés par les mêmes méchanismes et donc qu'il existe un rôle de la contrainte statique sur le déclenchement des glissements de terrain.

This work studies new algorithms and data structures that are useful in the context of program verification. As computers have become more and more ubiquitous in our modern societies, an increasingly large number of computer-based systems are considered safety-critical. Such systems are characterized by the fact that a failure or a bug (computer error in the computing jargon) could potentially cause large damage, whether in loss of life, environmental damage, or economic damage. For safety-critical systems, the industrial software engineering community increasingly calls for using techniques which provide some formal assurance that a certain piece of software is correct. One of the most successful program verification techniques is model checking, in which programs are typically abstracted by a finite-state machine. After this abstraction step, properties (typically in the form of some temporal logic formula) can be checked against the finite-state abstraction, with the help of automated tools. Alternating automata play an important role in this context, since many temporal logics on words and trees can be efficiently translated into those automata. This property allows for the reduction of model checking to automata-theoretic questions and is called the automata-theoretic approach to model checking. In this work, we provide three novel approaches for the analysis (emptiness checking) of alternating automata over finite and infinite words. First, we build on the successful framework of antichains to devise new algorithms for LTL satisfiability and model checking, using alternating automata. These algorithms combine antichains with reduced ordered binary decision diagrams in order to handle the exponentially large alphabets of the automata generated by the LTL translation. Second, we develop new abstraction and refinement algorithms for alternating automata, which combine the use of antichains with abstract interpretation, in order to handle ever larger instances of alternating automata. Finally, we define a new symbolic data structure, coined lattice-valued binary decision diagrams that is particularly well-suited for the encoding of transition functions of alternating automata over symbolic alphabets. All of these works are supported with empirical evaluations that confirm the practical usefulness of our approaches. / Ce travail traite de l'étude de nouveaux algorithmes et structures de données dont l'usage est destiné à la vérification de programmes. Les ordinateurs sont de plus en plus présents dans notre vie quotidienne et, de plus en plus souvent, ils se voient confiés des tâches de nature critique pour la sécurité. Ces systèmes sont caractérisés par le fait qu'une panne ou un bug (erreur en jargon informatique) peut avoir des effets potentiellement désastreux, que ce soit en pertes humaines, dégâts environnementaux, ou économiques. Pour ces systèmes critiques, les concepteurs de systèmes industriels prônent de plus en plus l'usage de techniques permettant d'obtenir une assurance formelle de correction. Une des techniques de vérification de programmes les plus utilisées est le model checking, avec laquelle les programmes sont typiquement abstraits par une machine a états finis. Après cette phase d'abstraction, des propriétés (typiquement sous la forme d'une formule de logique temporelle) peuvent êtres vérifiées sur l'abstraction à espace d'états fini, à l'aide d'outils de vérification automatisés. Les automates alternants jouent un rôle important dans ce contexte, principalement parce que plusieurs logiques temporelle peuvent êtres traduites efficacement vers ces automates. Cette caractéristique des automates alternants permet de réduire le model checking des logiques temporelles à des questions sur les automates, ce qui est appelé l'approche par automates du model checking. Dans ce travail, nous étudions trois nouvelles approches pour l'analyse (le test du vide) desautomates alternants sur mots finis et infinis. Premièrement, nous appliquons l'approche par antichaînes (utilisée précédemment avec succès pour l'analyse d'automates) pour obtenir de nouveaux algorithmes pour les problèmes de satisfaisabilité et du model checking de la logique temporelle linéaire, via les automates alternants.Ces algorithmes combinent l'approche par antichaînes avec l'usage des ROBDD, dans le but de gérer efficacement la combinatoire induite par la taille exponentielle des alphabets d'automates générés à partir de LTL. Deuxièmement, nous développons de nouveaux algorithmes d'abstraction et raffinement pour les automates alternants, combinant l'usage des antichaînes et de l'interprétation abstraite, dans le but de pouvoir traiter efficacement des automates de grande taille. Enfin, nous définissons une nouvelle structure de données, appelée LVBDD (Lattice-Valued Binary Decision Diagrams), qui permet un encodage efficace des fonctions de transition des automates alternants sur alphabets symboliques. Tous ces travaux ont fait l'objet d'implémentations et ont été validés expérimentalement.

La programmation par aspects est un paradigme de programmation qui permet de mieux séparer les préoccupations d'une application. Un aspect est défini pour chaque préoccupation qui ne peut pas être isolée dans un module. Les aspects sont ensuite ajoutés au programme de base par un processus automatique appelé tissage. Cependant, l'expressivité des langages d'aspect généraux permet de modifier totalement la sémantique du programme de base (par ex., un aspect peut remplacer certains appels de méthode par du code arbitraire). Ce comportement peut entraîner la perte des avantages (lisibilité, maintenabilité, réutilisabilité, etc.) d'une meilleure modularisation des préoccupations. Il devient impossible de raisonner sur le programme de base sans regarder le programme tissé. Cette thèse apporte une réponse aux problèmes ci-dessus en définissant des catégories d'aspects dont l'impact sur la sémantique du programme de base reste sous contrôle. Pour chaque catégorie d'aspects, nous déterminons l'ensemble des propriétés du programme de base qui est préservé par tissage. L'appartenance d'un aspect à une catégorie est garantie par construction grâce à des langages d'aspect dédiés pour chaque catégorie. L'utilisation de ces langages assure que le tissage préservera l'ensemble des propriétés associé à la catégorie concernée. Les propriétés préservées sont représentées comme des sous ensembles de LTL et de CTL*. Nous prouvons formellement que quelque soit le programme de base, le tissage de n'importe quel aspect d'une catégorie préserve les propriétés de la catégorie correspondante. Ces langages et catégories sont définis dans un cadre formel indépendant de tout langage de base ou d'aspect. L'expressivité de ce cadre est montrée en décrivant des primitives complexes de langages d'aspect comme AspectJ et CaesarJ et en effectuant une preuve de correction de transformation d'aspect.

Thèse doctorat : Informatique : Villeurbanne, INSA : 2006. / Titre provenant de l'écran-titre. Bibliogr. p. 207-213.