La symétrie est par définition un concept multidisciplinaire. Il apparaît dans de nombreux domaines. En général, elle revient à une transformation qui laisse invariant un objet. Le problème de satisfaisabilité (SAT) occupe un rôle central en théorie de la complexité. Il est le problème de décision de référence de la classe NP-complet (Cook, 71). Il consiste à déterminer si une formule CNF admet ou non une valuation qui la rend vraie. Dans la première contribution de ce mémoire, nous avons introduit une nouvelle méthode complète qui élimine toutes les symétries locales pour la résolution du problème SAT en exploitant son groupe des symétries. Les résultats obtenus montrent que l'exploitation des symétries locales est meilleure que l'exploitation des symétries globales sur certaines instances SAT et que les deux types de symétries sont complémentaires, leur combinaison donne une meilleure exploitation.En deuxième contribution, nous proposons une approche d'apprentissage de clauses pour les solveurs SAT modernes en utilisant les symétries. Cette méthode n'élimine pas les modèles symétriques comme font les méthodes statiques d'élimination des symétries. Elle évite d'explorer des sous-espaces correspondant aux no-goods symétriques de l'interprétation partielle courante. Les résultats obtenus montrent que l'utilisation de ces symétries et ce nouveau schéma d'apprentissage est profitable pour les solveurs CDCL.En Intelligence Artificielle, on inclut souvent la non-monotonie et l'incertitude dans le raisonnement sur les connaissances avec exceptions. Pour cela, en troisième et dernière contribution, nous avons étendu la notion de symétrie à des logiques non classiques (non-monotones) telles que les logiques préférentielles, les X-logiques et les logiques des défauts.Nous avons montré comment raisonner par symétrie dans ces logiques et nous avons mis en évidence l'existence de certaines symétries dans ces logiques qui n'existent pas dans les logiques classiques. / Symmetry is by definition a multidisciplinary concept. It appears in many fields. In general, it is a transformation which leaves an object invariant. The problem of satisfiability (SAT) is one of the central problems in the complexity theory. It is the first decision Np-complete problem (Cook, 71). It deals with determining if a CNF formula admits a valuation which makes it true. First we introduce a new method which eliminates all the local symmetries during the resolution of a SAT problem by exploiting its group of symmetries. Our experimental results show that for some SAT instances, exploiting local symmetries is better than exploiting just global symmetries and both types of symmetries are complementary. As a second contribution, we propose a new approach of Conflict-Driven Clause Learning based on symmetry. This method does not eliminate the symmetrical models as the static symmetry elimination methods do. It avoids exploring sub-spaces corresponding to symmetrical No-goods of the current partial interpretation. Our experimental results show that using symmetries in clause learning is advantageous for CDCL solvers.In artificial intelligence, we usually include non-monotony and uncertainty in the reasoning on knowledge with exceptions. Finally, we extended the concept of symmetry to non-classical logics that are preferential logics, X-logics and default logics. We showed how to reason by symmetry in these logics and we prove the existence of some symmetries in these non-classical logics which do not exist in classical logics.

Depuis l'antiquité jusqu'à aujourd'hui, le domaine de la logique a gagné une importance remarquable et contribue désormais à de nombreuses autres branches, telles que la philosophie, les mathématiques, la fabrication de matériel informatique, la linguistique, l'informatique, l'intelligence artificielle, etc. À chacun de ces scénarios correspondent des besoins spécifiques, qui vont d'exigences très concrètes, telles qu'une méthode d'inférence efficace, à des propriétés théoriques plus abstraites, telles qu'un système d'axiomes élégant. Étant donnée cette grande diversité d'utilisations, une palette hétéroclite de langages formels a été développée. Pendant de nombreuses années, les langages classiques (notamment la logique du premier ordre) étaient la seule alternative concevable, mais cet assortiment d'applications a rendu d'autres types de logiques également désirables dans de nombreuses situations. Imaginez que l'heure de choisir une logique pour une tâche spécifique arrive. Comment choisir la plus appropriée? Quelles propriétés devrions-nous rechercher? Comment "mesurer'' une logique par rapport aux autres? Ce sont des questions difficiles, et il n'existe pas de recette générale à suivre. Dans cette thèse, nous allons simplement restreindre ces questions à une famille particulière de logiques, et dans ce contexte, nous explorerons les aspects théoriques qui aideront à répondre à ces préoccupations. Beaucoup peut être découvert par une analyse attentive des cas les plus intéressants, et notre contribution sera développée selon cette philosophie. Les logiques modales propositionnelles offrent une alternative aux langages traditionnels. Elles peuvent être considérées comme un ensemble d'outils permettant de concevoir des logiques adaptées à des tâches précises, possédant un contrôle fin sur leur expressivité. De plus, il s'est avéré que les logiques modales possèdent un bon comportement computationnel, qui se trouve être robuste y compris malgré l'ajout d'extensions. Ces caractéristiques, parmi d'autres, ont élevé les logiques modales au rang d'alternatives désirables aux langages classiques. Dans ce thèse, nous allons présenter une nouvelle famille de logiques modales appelée logiques mémorielles. Les logiques modales traditionnelles permettent de décrire les structures relationnelles d'un point de vue local. Mais pourquoi ne pas changer cette structure? Nous voulons étudier l'ajout d'une structure de stockage explicite aux logiques modales, une mémoire, qui permet de modéliser un comportement dynamique à travers des opérateurs mémoriels explicites. Ces opérateurs sauvent ou restaurent de l'information vers et à partir de la mémoire. Naturellement, selon le type de structure de sauvegarde désiré et les opérateurs mémoriels disponibles, la logique résultante possèdera différentes propriétés qui valent la peine d'être étudiées. Cette thèse est organisée de la façon suivante. Dans le Chapitre 1, nous commençons par rappeler brièvement comment la logique modale est née, en montrant les différents points de vue historiques la concernant. Puis, nous présentons formellement la logique modale de base et un ensemble d'opérateurs étendus qui aident à capturer le ``goût'' modal de langages plus riches. Nous finissons ce chapitre en donnant un premier aperçu des logiques mémorielles, et montrons comment elles peuvent aider à modéliser l'état quand nous choisissons d'utiliser un ensemble comme une structure de sauvegarde. Le Chapitre 2 est dédié à la présentation détaillée des logiques mémorielles. Nous montrons quelques exemples qui peuvent être décrits en ajoutant un ensemble à des structures relationnelles usuelles, ainsi que les opérateurs ensemblistes usuels permettant l'ajout d'élément et le test d'appartenance. Puis, nous montrons que d'autres opérateurs mémoriels peuvent être envisagés, et nous discutons de la possibilité d'ajouter des contraintes à l'interaction entre la mémoire et les opérateurs modaux. Ces contraintes peuvent être vues comme une manière d'avoir un contrôle fin sur l'expressivité de la logique. Comme nous avons fait des changements aux logiques modales classiques, nous nous intéressons à l'analyse de l'impact de ces changements sur les logiques résultantes. Ainsi, le reste de ce chapitre présente une boite à outils logique basique avec laquelle nous pouvons analyser cette nouvelle famille de logiques. Cette boite à outils peut être vue comme un plan qui organise le reste de cette thèse et qui permet d'analyser les logiques mémorielles en termes d'expressivité, de complexité, d'interpolation et de théorie de la preuve. Le reste des chapitres consiste à étudier en détail chacun de ces aspects. Dans les Chapitres 3 et 4, nous explorons l'expressivité de plusieurs logiques mémorielles et nous étudions la décidabilité de leur problème de satisfiabilité. Dans les cas décidables, nous déterminons leur complexité. Nous analysons l'impact des différents opérateurs mémoriels considérés, et leur interaction. Nous étudions également d'autres conteneurs mémoriels, tels que la pile. Puis, dans le Chapitre 4, nous analysons l'interpolation de Craig et la définabilité de Beth pour certains fragments des logiques mémorielles. Nous étudions également les logiques mémorielles du point de vue de la théorie de la preuve. Dans les Chapitres 6 et 7, nous passons aux axiomatisations à la Hilbert et aux systèmes de tableaux, et nous caractérisons plusieurs fragments de la famille des logiques mémorielles, en utilisant principalement des techniques empruntées aux logiques hybrides. Nous concluons dans le Chapitre 8 avec quelques remarques, des problèmes ouverts et des directions pour de futures recherches. / From ancient times to the present day, the field of logic has gained significant strength and now it actively contributes to many different areas, such as philos- ophy, mathematics, linguistic, computer science, artificial intelligence, hardware manufacture, etc. Each of these scenarios has specific needs, that range from very concrete requirements, like an efficient inference method, to more abstract theoretical properties, like a neat axiomatic system. Given this wide diversity of uses, a motley collection of formal languages has been developed. For many years, classical languages (mainly classical first order logic) were the alternative, but this assortment of applications made other types of logics also attractive in many situations. Imagine that the time for choosing a logic for some specific task arrives. How can we decide which is the one that fits best? Which properties should we look for? How can we “measure” a logic with respect to others? These are not easy questions, and there is not a general recipe one can follow. In this thesis we are just going to restrict these questions to a particular family of logics, and in that context we will investigate theoretical aspects that help to answer some of these concerns. Much can be discovered by carefully analyzing appealing cases, and our contribution will be developed having that philosophy in mind. Propositional modal logics offer an alternative to traditional languages. They can be regarded as a set of tools that allow to design logics specially tailored for specific tasks, having a fine-grained control on their expressivity. Additionally, modal logics turned out to have a good computational behavior, which proved to be quite robust under extensions. These characteristics, among others, placed modal logics as an attractive alternative to classical languages. In this dissertation we are going to present a new family of modal logics called memory logics. Traditional modal logics enables to describe relational structures from a local perspective. But what about changing the structure? We want to explore the addition of an explicit storage structure to modal logics, a mem- ory, that allows to model dynamic behavior through explicit memory operators. These operators store or retrieve information to and from the memory. Natu- rally, depending on which type of storage structure we want, and which memory operators are available, the resulting logic will enjoy different properties that are worth investigating. The thesis is organized as follows. In Chapter 1 we start by giving a brief recap of how modal logic was born, showing the different historical perspectives used to look at modal logic. Then we formally present the basic modal logic and a set of extended operators that helps grasp the modal “flavor” of some richer languages. We finish this chapter by giving a first glance of memory logics, and showing how they can help to model state when we choose to use a set as storage structure. Chapter 2 is devoted to present memory logics in detail. We show some examples that can be described by adding a set to standard relational structures, and the usual set operators to add elements and test membership. We then show some other memory operators that can be considered, and we discuss the possibility of adding constraints to the interplay between memory and modal operators. These constraints can be regarded as a way to have a finer-grained control on the logic expressivity. Since we have made changes to classical modal logics, we are interested in analyzing the impact those changes cause in the resulting logics. Therefore, the rest of this chapter presents a basic logic toolkit through which we can analyze this new family of logics. This toolkit can be seen as an outline that organizes the rest of the thesis and that allows to analyze memory logics in terms of expressivity, complexity, interpolation and proof theory. The rest of the chapters investigate each of these aspects in detail. In Chap- ters 3 and 4 we explore the expressive power of several memory logics and we study the decidability of their satisfiability problem. In the decidable cases, we determine their computational complexity. We analyze the impact of the differ- ent memory operators we consider, and how they interact. We also study other memory containers, such as a stack. Then, in Chapter 5, we analyze Craig inter- polation and Beth definability for some memory logic fragments. We also study memory logics from a proof theoretical perspective. In Chapter 6 and 7 we turn to Hilbert style axiomatizations and tableau systems, and we characterize several fragments of the memory logic family mostly using techniques borrowed from hy- brid logics. We close in Chapter 8 with some concluding remarks, open problems and directions for further research.

Le transcodage est un élément clé dans la transmission vidéo permettant à une séquence vidéo de passer d'un type de codage à un autre afin de s'adapter au mieux aux capacités de transport d'un canal de transmission. L'intérêt de ce type de traitement est de faire profiter un maximum d'utilisateurs possédant des terminaux variés dont la résolution spatiale, la résolution temporelle affichable, et le type de canal utilisé pour accéder au média varient fortement, et cela à partir d'une seule source de qualité et résolution maximale, stockée sur un serveur, par exemple. Le transcodage est adapté dans les cas où l'on souhaite envoyer une séquence vidéo vers un destinataire et dont le chemin serait constitué de divers canaux de transmission. Nous avons réalisé un transcodeur par requantification ainsi qu'un transcodeur par troncature. Ces deux méthodes ont été comparées et il apparait qu'en termes de qualité d'image l'une ou l'autre de ces méthodes est plus efficace selon le contexte. La suite de nos travaux consiste en l'étude du standard scalable dérivé de H.264 AVC, le standard SVC (Scalable Video Coding). Nous avons souhaité étudier un transcodeur en qualité, mais aussi en résolution spatiale qui permettra de réécrire le flux SVC en un flux AVC décodable par les décodeurs du marché actuel. Cette transposition est réalisée grâce à une architecture reconfigurable permettant de s'adapter aux nombreux types de flux pouvant être conformes au standard SVC d' H.264. L'étude proposée a aboutie à une implémentation partielle d'un transcodeur du type SVC vers AVC. Nous proposons dans cette thèse une description des implémentations de transcodage concernant les formats AVC puis SVC / Transcoding is a key element in the video transmission allows a video to go from one encoding type to another in order to adapt better to the transport capacity of a transmission channel. The advantage of this type of treatment is to make the most of users with various terminals with spatial resolution, temporal resolution displayable, and type of channel used to access the media vary widely, and from that of a single source of quality and maximum resolution, stored on a server, for example. Transcoding is appropriate where you want to send a video to a recipient and whose path would consist of various transmission channels. We realized by a transcoder and a requantization transcoder by truncation. These two methods were compared and it appears that in terms of image quality in either of these methods is more effective depending on the context. Following our work is the study of the standard H.264 AVC scalable derivative of the standard SVC (Scalable Video Coding). We wanted to study as a transcoder, but also in spatial resolution which will rewrite the SVC flow in a stream stroke decodable by decoders on the market today. This mapping is achieved through are configurable architecture to adapt to many types of flow which may conform to standard SVC to H.264. The proposed study has accomplished a partial implementation of a transcoder type SVC to AVC. We propose here a description of the implementations on AVC transcoding and SVC

Comme les syst`emes mat´eriels et logiciels grandissent de fa¸con continue en ´echelle et fonctionnalit´es, la probabilit´e d’erreurs subtiles de- vient toujours plus grande. Les techniques d’abstraction, souvent bas´ees sur l’interpr´etation abstraite de Cousot, fournissent une m´ethode pour ex´ecuter symboliquement les syst`emes en utilisant le domaine abstrait `a la place du domaine concret. Dans cette th`ese, on introduit des techniques d’abstraction pour les logiques sous des interpr´etations multi-valu´ees. Beaucoup d’applications des logiques multi-valu´ees ont ´et´e trouv´ees dans la v´erification du mat´eriel et du logiciel. Pour la v´erification du mat´eriel, des outils de simulation et des r´ealisations des circuits multi-valu´es v´eritables ont ´et´e propos´es, les risques dynamiques ont ´et´e model´es en introduisant des ´etats faux pour trouver des r´egions chevauchantes des signaux en concurrence, etc. Pour la v´erification du logiciel on a besoin d’incertitude parce qu’on ne peut savoir si certains comportements devraient ˆetre possibles et on a besoin du d´esaccord parce que l’on peut avoir des acteurs diff´erents qui sont en d´esaccord pour la mani`ere dont les syst`emes devraient se comporter. Les abstractions sont obtenues en appliquant des relations d’´equivalence et apr`es, les symboles pr´edicatifs de la logique sont red´efinis `a s’appliquer cor- rectement aux classes d’´equivalence `a l’aide des politiques d’interpr´etation. On fournit des r´esultats de pr´eservation pour la logique de premier ordre, pour la logique temporelle et pour la logique temporelle de la connaissance. Avant de discuter les abstractions multi-valu´ees pour la logique temporelle, nous pr´esentons une ´etude de cas pour utiliser l’abstraction dans le contexte des mod`eles du contrˆole d’acc`es. Nous fournirons aussi une technique d’abstraction pour les types de do- nn´ees. Cette technique d’abstraction peut ˆetre ´elargie pour les types abstraits de donn´ees. Ici, les abstractions sont appliqu´ees aux sp´ecifications initiales au moyen des ´equations et ils sont appel´es des abstractions ´equationnelles. De plus, la technique d’abstraction pr´esent´ee g´en´eralise et clarifie la nature de beaucoup de techniques d’abstraction trouv´ees dans la litt´erature, telles: la technique de dupliquer les symboles pr´edicatifs, shape analysis, l’abstraction par pr´edicats, l’approche de McMillan, etc. Pour raisonner au sujet des syst`emes dynamiques, on introduit les types de donn´ees dynamiques et on ´etend la m´ethode d’abstraction ant´erieure `a ce cas. Le probl`eme principal qui survient quand on utilise les abstractions est de trouver l’abstraction convenable ou de raffiner une abstraction d´ej`a existante pour en obtenir une meilleure. On prouve que les techniques d’abstraction que nous avons introduites pour les types de donn´ees sous l’interpr´etation 3- valu´ee Kleene, peuvent ˆetre utilis´ees dans une proc´edure de raffinement. De plus, on montre que la proc´edure de raffinement guid´e par contre-exemple est plus efficace quand on l’utilise sous les abstractions ´equationnelles / As the hardware and software systems are growing continuously in scale and functionality, the likelihood of subtle errors becomes greater. Abstraction techniques, often based on abstract interpretation, provide a method for symbolically executing systems using the abstract instead of the concrete domain. In this thesis, we are concerned with abstractions for logics under multi-valued interpretations. Many applications of multi-valued logics have been found in hardware and software verification. For hardware verification, simulation tools and imple- mentations of genuinely multi-valued circuits have been proposed, dynamic hazards have been modeled by introducing pseudo states to find overlapping regions of competing signals, implementation of gates have been verified on the basis of switch level models, etc. For software verification, we need uncer- tainty because we may not know whether some behaviors should be possible, we need disagreement because we may have different stakeholders that dis- agree about how the systems should behave and we need to represent relative importance because some behaviors are essential and others may or may not be implemented. The abstractions are obtained by applying equivalence relations and then, the predicate symbols of the logic are re-defined to work properly on equiva- lence classes by using interpretation policies. We provide preservation results for first-order logic, temporal logic, and temporal logic of knowledge. As a case study, we show how abstraction can be used to solve the safety problem for protection systems which model access control policies. The use of abstraction in the context of data types, is also investigated. This technique scales well from data types to abstract data types. Here, abstractions are applied to initial specifications by means of equations and they are called equationally specified abstractions. Moreover, the abstraction technique we propose generalizes and clarifies the nature of many abstraction techniques found in the literature, such as the technique of duplicating pred- icate symbols, shape analysis, predicate abstraction, McMillan’s approach, etc. To reason about dynamic systems, we introduce dynamic data types and extend the previous abstraction technique to this case. The main problem that arises when using abstraction techniques is to find the suitable abstraction or to refine an already existing abstraction in order to obtain a better one. In this thesis, we prove that the abstraction techniques for data types, under Kleene’s three-valued interpretation, can be used in a refinement procedure. Moreover, we show that the counterexample guided abstraction refinement procedure (CEGAR) works better when used with equationally specified abstractions

Cette étude porte sur l'architecture globale d'un agent rationnel. Le terme agent est donne aux systèmes autonomes, c'est a dire capables d'agir sans intervention extérieure. De plus, l'hypothèse qu'il est rationnel est faite, c'est a dire que l'ensemble de ses activités extérieures, perceptives et déductives sont justifiables par ses buts. La spécification et l'implantation sont décrites

Reproduction de : Thèse de doctorat : Génie électrique : Toulouse, INPT : 2003. / Titre provenant de l'écran-titre. Bibliogr. 36 réf.

Reproduction de : Thèse de doctorat : Génie électrique : Toulouse, INPT : 2002. / Titre provenant de l'écran-titre. Bibliogr. 77 réf.

Reproduction de : Thèse de doctorat : informatique : Grenoble, INPG : 1988. / Titre provenant de l'écran-titre. Bibliogr. p. 167-173.

Thèse de doctorat : Instrumentation et Micro-Électronique : Nancy 1 : 2008. / Titre provenant de l'écran-titre. Bibliogr.

Thèse de doctorat : Génie électrique : Nancy 1 : 2009. / Titre provenant de l'écran-titre.