Two-player zero-sum games of infinite duration and their quantitative versions are used in verification to model the interaction between a controller (Eve) and its environment (Adam). The question usually addressed is that of the existence (and computability) of a strategy for Eve that can maximize her payoff against any strategy of Adam: a winning strategy. It is often assumed that Eve always knows the exact state of the game, that is, she has full observation. In this dissertation, we are interested in two variations of quantitative games. First, we study a different kind of strategy for Eve. More specifically, we consider strategies that minimize her regret: the difference between her actual payoff and the payoff she could have achieved if she had known the strategy of Adam in advance. Second, we study the effect of relaxing the full observation assumption on the complexity of computing winning strategies for Eve. Regarding regret-minimizing strategies, we give algorithms to compute the strategies of Eve that ensure minimal regret against three classes of adversaries: (i) unrestricted, (ii) limited to positional strategies, or (iii) limited to word strategies. These results apply for quantitative games defined with the classical payoff functions Inf, Sup, LimInf, LimSup, mean payoff, and discounted sum. For partial-observation games, we continue the study of energy and mean- payoff games started in 2010 by Degorre et al. We complement their decidability result for a particular problem related to energy games (the Fixed Initial Credit Problem) by giving tight complexity bounds for it. Also, we show that mean-payoff games are undecidable for all versions of the mean-payoff function. Motivated by the latter negative result, we define and study several decidable sub-classes of mean-payoff games. Finally we extend the newly introduced window mean-payoff objectives to the partial observation setting. We show that they are conservative approximations of partial-observation mean-payoff games and we classify them according to whether they are decidable. Furthermore, we give a symbolic algorithm to solve them. / Doctorat en Sciences / info:eu-repo/semantics/nonPublished

En raison de leur propriétés spécifiques élevées, par rapports aux alliages légers, les Composites à matrice métallique (CMM) représentent des matériaux d'intérêt pour des applications de haute technologie dans les domaines aéronautique et aérospatiale. Les CMM les plus couramment utilisés sont à renfort particulaire, ou PRMMC, et à matrice Al en raison de leur faible densité. Cette thèse porte sur la mise au point de PRMMC à renfort nanométrique par une voie de synthèse réactive globale. En raison des normes encadrant l’usage des nanomatériaux et visant à limiter l’exposition des usagers et de l’environnement, la manipulation de poudres de taille nanométrique est coûteuse et problématique dans le cadre d’un usage industriel. La nouvelle voie de synthèse qui a été développée dans le cadre de cette thèse a permis de démontrer la faisabilité de composites à matrice métallique et à renfort particulaire nanométrique, dimension moyenne de 30 nm, sans avoir recourt initialement à des poudres de taille nanométrique. Le procédé étudié consiste en une réaction chimique à haute température entre deux matériaux précurseurs qui conduit à la formation in-situ non seulement du renfort mais aussi de la matrice. Par rapport aux techniques de synthèse classiques, cette technique permet de synthétiser des nanoparticules in situ et d’en contrôler la taille. De plus, la matrice et le renfort étant co produits par la réaction à haute température, l’interface entre les deux phases est exempte de couches d’oxydes, ce qui lui assure une très bonne adhésion. Dans le cadre du projet ANR NanoTiCAl, la faisabilité de cette nouvelle méthode a été étudiée à travers le cas d'un composite à matrice aluminium renforcé par des particules de carbure de titane (TiC). Les synthèses ont été réalisées entre 900°C et 1000°C à partir d’un couple de précurseurs incluant le graphite et un aluminiure de titane (Al3Ti). Le composite obtenu, caractérisé par un taux de renfort élevé de 34wt.%, possède un module de Young de 106 GPa, un allongement maximal à la rupture de 6% ainsi qu’une énergie à rupture de l’ordre de 28 J.cm-3. Ces valeurs démontrent un compromis entre résistance et capacité d’endommagement original et particulièrement intéressant, jamais observé dans la littérature pour des composites d’une teneur en renfort aussi importante. La caractérisation fine de la microstructure du composite ainsi que du renfort TiC après extraction du composite massif, ont permis de mieux comprendre les mécanismes à l’oeuvre dans cette voie de synthèse réactive. Enfin, sur la base de la compréhension obtenue dans le cas du composite Al/TiC, des critères ont été identifiés permettant d’aller vers une généralisation de ce procédé de synthèse. La pertinence de cette généralisation a finalement pu être démontrée par quelques mises en application à d’autres systèmes / Metal Matrix Composites (MMCs) have attracted research and industrial attentions as materials for high technological applications in the aeronautic and aerospace industry. The MMCs differ by their high specific mechanical properties compared to light weight alloys. The most commonly used are the Particulate Reinforcement Metal Matrix Composites (PRMMCs), especially the Al based matrices because of their low density.This thesis deals with the reactive synthesis of PRMMCs reinforced by nanoparticles. Because of the standards governing the use of nanomaterials to limit the exposure of users and environment, handling nanoscaled powders is very problematic and expensive in industry. Furthermore, the cost of this kind of processes is very high. This new synthesis route, developed during this thesis, shows the feasibility of PRMMCs reinforced by nanosized particles, with a mean size of 30 nm, without using any starting nanoparticles.The process consists in a chemical reaction at high temperature between precursor materials which leads to form both of the matrix and the reinforcement phase. Compared to conventional synthesis techniques as stir casting, this route allows to synthesis nanoparticles in-situ and to control their size. In addition, the matrix and the reinforcement, which are formed by a reaction at high temperature, have an interface free of oxide layers which assures a good adhesion.In the NanoTiCAl project, the feasibility of this new method is illustrated in the case of an aluminium based composite reinforced by titanium carbide (TiC). The synthesis were realized between 900°C and 1000°C from a couple of precursors including graphite and titanium aluminide (Al3Ti). The resulting composite, characterized by a high reinforcement ratio (34 wt.%), presents a Young’s modulus of 106 GPa, a maximum elongation of 6 % and a high toughness, about 28 J.cm-3. These values represent an uncommon compromise between strength and toughness never seen in the literature regarding to the high content of reinforcement.The characterization of the composite microstructure and of the reinforcement phase, after extraction of the solid composite, allowed a better understanding of the reaction mechanism during the reactive synthesis. Finally, based on our understanding of the Al-TiC composite, criteria have been identified to generalize this synthesis process. This generalization was demonstrated with success in other systems

Depuis les années 70, les oxydes mixtes de type hexaaluminate suscitent un intérêt certain pour les réactions catalytiques du fait de leur stabilité thermique élevée qui leur confère un fort potentiel pour les réactions à haute température. Cependant, la majorité des procédés de synthèse adoptés pour la préparation de ces derniers nécessite au moins une étape de traitement thermique à haute température afin d'achever le processus de cristallisation. Ainsi, les hexaaluminates préparées par voie chimique classique présentent des tailles de particules larges et des aires spécifiques réduites (< 20 m2 g-1). Dans le cadre de ce travail, l'optimisation des paramètres et des conditions de synthèse pour la préparation d'hexaaluminate nanocristalline de grande aire spécifique a fait l'objet d'une étude détaillée. Le broyage réactif s'est révélé être une méthode de synthèse efficace, et des aires spécifiques très élevées ont été obtenues (> 70 m2 g-1). Il a été observé que la nature et la concentration du métal de transition inséré dans la structure influence fortement les propriétés redox et la mobilité d'oxygène de ces solides. Cependant, pour une même composition chimique, les propriétés redox et la mobilité de l'oxygène sont conditionnées par les propriétés structurales et texturales. L'étude des propriétés catalytique des hexaaluminates en oxydation de CH4 et de CO a montré que l'activité de ces derniers résulte d'un équilibre complexe entre les propriétés texturales et structurales, l'état de la surface (nature et concentration des sites redox), et les propriétés de réductibilité et de mobilité d'oxygène. / Since the beginning of the 1970's, hexaaluminate mixed oxides gained were studied as active materials for catalytic reaction at high temperature, e.g. catalytic combustion. Their abilities to maintain phase stability and high surface area are considered of a great interest. Unfortunately, most of the reported chemical synthesis methods for hexaaluminate preparation involve at least one calcination step at high temperature (> 1100 °C) to crystallize the desired pure phase, which leads to crystal growth and unavoidable surface reduction.The catalytic performance of hexaaluminate materials depends essentially to the structural and textural properties i.e. surface area, crystal size, and phase purity. Thus the first part of this study was dedicated to the development of an original synthesis route, the "Activated Reactive Synthesis" process that is evidenced as a promising top down approach to generate nanostructured hexaaluminate with high surface area. Values of surface areas obtained were largely higher (>77 m2 g-1) to those reported for hexaaluminates prepared by conventional routes (~ 20 m2 g-1). The nature of the transition metal Mn+ inserted in the hexaaluminate structure, as well as its concentration, plays a key role on the redox behaviours and the oxygen transfer properties. Nevertheless, for a same chemical composition, the redox properties and oxygen mobility was found to be dependent to the structural and textural properties. Activities of hexaaluminate materials in oxidation reaction of CO and CH4 is reported to depend on a complex balance between structural and textural properties, surface state, reducibility, and oxygen mobility in the bulk.

A reactive system is a system that continuously interacts with its environment. The environment provides an input signal, to which the system reacts with an output signal, and so on ad infinitum. In reactive synthesis, the goal is to automatically generate an implementation from a specification of the reactive and non-terminating input/output behaviours of a system. In the classical setting, the set of signals is assumed to be finite. however, this assumption is not realistic to model systems which process sequences of signals accompanied with data from a possibly infinite set (e.g. a client id, a sensor value, etc.), which need to be stored in memory and compared against each other.The goal of this thesis is to lift the theory of reactive system synthesis over words on a finite alphabet to data words. The data domain consists in an infinite set whose structure is given by predicates and constants enriched with labels from a finite alphabet. In this context, specifications and implementations are respectively given as automata and transducers extended with a finite set of registers that they use to store data values. To determine the transition to take, they compare the input data with the content of the registers using the predicates of the domain.In a first part, we consider both the bounded and unbounded synthesis problem; the former additionally asks for a bound on the number of registers of the implementation, along with the specification. We do so for different instances, depending on whether the specification is a nondeterministic, universal (a.k.a. co-non-deterministic) or deterministic automaton, for various domains.While the bounded synthesis problem is undecidable for non-deterministic specifications, we provide a generic approach consisting in a reduction to the finite alphabet case, that is done through automata-theoretic constructions. This allows to reprove decidability of bounded synthesis for universal specifications over (ℕ,=), and to obtain new ones, such as the case of a dense order, or the ability of data guessing, all with a 2-ExpTime complexity.We then move to the unbounded synthesis problem, which is undecidable for specifications given by non-deterministic and universal automata, but decidable and ExpTime-complete for deterministic ones over (ℕ,=) and (ℚ,<). We also exhibit a decidable subclass in the case of (ℕ,<), namely one-sided specifications.In a second part, we lift the reactivity assumption, considering the richer class of implementations that are allowed to wait for additional input before reacting, again over data words. Specifications are modelled as non-deterministic asynchronous transducers, that output a (possibly empty) word when they read an input data. Already in the finite alphabet case, their synthesis problem is undecidable.A way to circumvent the difficulty is to focus on functional specifications, for which any input sequence admits at most one acceptable output. Targeting programs computed by input-deterministic transducers is again undecidable, so we shift the focus to deciding whether a specification is computable, in the sense of the classical extension of Turing-computability to infinite inputs. We relate this notion with that of continuity for the Cantor distance, which yields a decidable characterisation of computability for functional specifications given by asynchronous register transducers over (ℕ,=) and for the superseding class of oligomorphic data domains, that also encompasses $(ℚ,<)$. The study concludes with the case of (ℕ,<), that is again decidable. Overall, we get PSpace-completeness for the problems of deciding computability and refined notions, as well as functionality. / Option Informatique du Doctorat en Sciences / info:eu-repo/semantics/nonPublished