Abstractions are widely used in building reliable distributed systems as they simplifies the task of building complex systems and aid in reasoning about them. Implementing these abstractions, however, requires making certain assumptions about the environment in which they will be used. We find that there is a mismatch in the set of assumptions used to implement abstractions in the different layers of a distributed system. This leads to a costlier design and may render the implementation unusable in situations where the assumptions do not hold. In this dissertation we provide alternative implementations for the abstractions of distributed registers and communication channels that rely on a unified set of assumptions across the different layers of a distributed system. / text

Cette thèse revisite les problèmes d'accessibilité et de vivacité pour les au-tomates temporisés.L'accessibilité est couramment résolue par le calcul d'un arbre de recherche abstrait. L'abstraction est paramétrée par des bornes provenant des gardes de l'automate. Nous montrons que l'abstraction a 4LU de Behrmann et al. est la plus grande abstraction saine et complète pour les bornes LU. N' étant pas convexe, elle n'est pas mise en oeuvre dans les outils. Nous introduisons une méthode qui permet son utilisation éfficace. Finalement, nous proposons une optimisation des bornes à la volée exploitant le calcul de l'arbre.Le problème de vivacité requiert de détecter les exécutions Zenon/non-Zenon. Une solution standard ajoute une horloge à l'automate. Nous montrons qu'elle conduit a une explosion combinatoire. Nous proposons une solution qui évite ce problème pour une grande classe d'abstractions. Pour les abstractions LU nous montrons que détecter ces exécutions est un problèmeNP-complet. / We consider the classic model of timed automata introduced by Alurand Dill. Two fundamental properties one would like to check in this modelare reachability and liveness. This thesis revisits these classical problems.The reachability problem for timed automata asks if there exists a run ofthe automaton from the initial state to a given final state. The standard solutionto this problem constructs a search tree whose nodes are abstractionsof zones. For effectiveness, abstractions are parameterized by maximal lowerand upper bounds (LU-bounds) occurring in the guards of the automaton.Such abstractions are also termed as LU-abstractions. The a4LU abstractiondefined by Behrmann et al is the coarsest known LU-abstraction. Althoughit is potentially most productive to use the a4LU abstraction, it has not beenused in implementations as it could lead to non-convex sets. We show howone could use the a4LU abstraction efficiently in implementations. Moreover,we prove that a4LU abstraction is optimal: given only the LU-bound information,it is the coarsest possible abstraction that is sound and completefor reachability. We then concentrate on ways to get better LU-bounds. Inthe standard procedure the LU-bounds are obtained from a static analysisof the automaton. We propose a new method to obtain better LU-boundson-the-fly during exploration of the zone graph. The potential gains of proposedimprovements are validated by experimental results on some standardverification case studies.The liveness problem deals with infinite executions of timed automata.An infinite execution is said to be Zeno if it spans only a finite amountof time. Such runs are considered unrealistic. While considering infiniteexecutions, one has to eliminate Zeno runs or dually, find runs that arenon-Zeno. The B¨uchi non-emptiness problem for timed automata asks ifthere exists a non-Zeno run visiting an accepting state infinitely often. Thestandard solution to this problem adds an extra clock to take care of non-Zenoness. We show that this solution might lead to an exponential blowupin the search space. We propose a method avoiding this blowup for a wideclass of abstractions weaker than LU-abstractions. We show that such amethod does not exist for LU-abstractions unless P=NP. Another questionrelated to infinite executions of timed automata is to decide the existenceof Zeno runs. We provide the first complete solution to this problem. Itworks for a wide class of abstractions weaker than LU. Yet again, we showthe solution could lead to a blowup for LU-abstractions, unless P=NP.

This thesis is concerned with policy space abstractions that concisely encode alternative ways of making decisions; dealing with discovery, learning, adaptation and use of these abstractions. This work is motivated by the problem faced by autonomous agents that operate within a domain for long periods of time, hence having to learn to solve many different task instances that share some structural attributes. An example of such a domain is an autonomous robot in a dynamic domestic environment. Such environments raise the need for transfer of knowledge, so as to eliminate the need for long learning trials after deployment. Typically, these tasks would be modelled as sequential decision making problems, including path optimisation for navigation tasks, or Markov Decision Process models for more general tasks. Learning within such models often takes the form of online learning or reinforcement learning. However, handling issues such as knowledge transfer and multiple task instances requires notions of structure and hierarchy, and that raises several questions that form the topic of this thesis – (a) can an agent acquire such hierarchies in policies in an online, incremental manner, (b) can we devise mathematically rigorous ways to abstract policies based on qualitative attributes, (c) when it is inconvenient to employ prolonged trial and error learning, can we devise alternate algorithmic methods for decision making in a lifelong setting? The first contribution of this thesis is an algorithmic method for incrementally acquiring hierarchical policies. Working with the framework of options - temporally extended actions - in reinforcement learning, we present a method for discovering persistent subtasks that define useful options for a particular domain. Our algorithm builds on a probabilistic mixture model in state space to define a generalised and persistent form of ‘bottlenecks’, and suggests suitable policy fragments to make options. In order to continuously update this hierarchy, we devise an incremental process which runs in the background and takes care of proposing and forgetting options. We evaluate this framework in simulated worlds, including the RoboCup 2D simulation league domain. The second contribution of this thesis is in defining abstractions in terms of equivalence classes of trajectories. Utilising recently developed techniques from computational topology, in particular the concept of persistent homology, we show that a library of feasible trajectories could be retracted to representative paths that may be sufficient for reasoning about plans at the abstract level. We present a complete framework, starting from a novel construction of a simplicial complex that describes higher-order connectivity properties of a spatial domain, to methods for computing the homology of this complex at varying resolutions. The resulting abstractions are motion primitives that may be used as topological options, contributing a novel criterion for option discovery. This is validated by experiments in simulated 2D robot navigation, and in manipulation using a physical robot platform. Finally, we develop techniques for solving a family of related, but different, problem instances through policy reuse of a finite policy library acquired over the agent’s lifetime. This represents an alternative approach when traditional methods such as hierarchical reinforcement learning are not computationally feasible. We abstract the policy space using a non-parametric model of performance of policies in multiple task instances, so that decision making is posed as a Bayesian choice regarding what to reuse. This is one approach to transfer learning that is motivated by the needs of practical long-lived systems. We show the merits of such Bayesian policy reuse in simulated real-time interactive systems, including online personalisation and surveillance.

L'objectif de cette étude est de proposer une approche générale d'évaluation de la validité d'une Modélisation et Simulation (M&S) utilisée dans le cadre du développement des systèmes embarqués. Cette approche s'inscrit dans une démarche visant à améliorer la confiance en l'utilisation d'une simulation dont les résultats sont souvent remis en cause sans justification cohérente. Le cadre d'application de l'étude est l'ensemble des produits de simulation d'Airbus. Au regard d'un objectif de validation d'un système, une simulation doit être la plus proche possible du système qu'elle représente. Dans le cycle de développement d'un avion, les simulations doivent être disponibles avant les systèmes eux-mêmes. Si le niveau de validité est trop faible les résultats nécessaires à l'expérience ne peuvent être atteints. Si le niveau de validité est trop élevé, du temps de travail de modélisation et de calcul est inutilement dépensé. Nous avons assimilé le problème de niveau de validité à une hiérarchie d'abstraction de modèles. Nous proposons un modèle de description des propriétés d'abstractions qui permet de parler strictement des mêmes choses lorsque le terme de "validité" est évoqué et d'évaluer la compatibilité entre un niveau de validité attendu par l'expérience et un niveau de validité fourni par le produit de simulation. Puis, nous avons établi des règles formelles de mise en correspondance d'un objectif d'utilisation et du domaine d'usage d'un modèle. Le problème de la mise en correspondance est fondé sur le principe qu'un objectif d'utilisation et un domaine d'usage d'une simulation sont deux composants, au sens formel du terme. Nous avons adapté les techniques de l'ingénierie basée composants, pour enrichir, par des techniques itératives, nos deux composants. Enfin nous avons proposé une méthodologie permettant d'intégrer nos concepts formels au processus d'Ingénierie Systèmes. Nous illustrons cette démarche sur un système de communication avionique.

Building models, whether to explain or to predict observed data, is an exercise of describing how the values of observed variables depend on those of others. Black box models only describe relationships between observed variables, and they are evaluated by their ability to accurately describe the values of observed variables in new situations not previously available to the model–such as the output response to a new set of inputs, for example. Black box models describe the observed behavior of the underlying system, but they may not correctly describe the way in which the system computes this behavior. White box models, on the other hand, describe the observed behavior and also incorporate hidden, intermediate variables that are used to describe the specific computation the underlying system uses to generate its observed behavior. In this sense, we say the white box model captures the structure of the system, in addition to its observed behavior. Since a given white box model may be accurately described by an infinite variety of black box models, all computing the same observed behavior but using different structures to do so, we say that any of these black box models is an abstraction of the white box model. This thesis constructs foundational pieces of a unifying theory of linear mathematical abstractions that are central to scientific modeling. It offers a precise description of the spectrums of grey box models linking any white and black box representation. There are various motivations for having this rich variety of representations of a given system. One key motivation is that of consilience, that is, to deepen our understanding of the modeling process by connecting various well developed theories under the umbrella of a broader theory. This work offers a precise relationship between Mason’s signal flow graphs [34] and Willem’s behavioral systems theory [66], in addition to linking the classical transfer function theory used by Nyquist [44], Bode [3], and Weiner [65] to the state space theory preferred by Kalman [27]. Another motivation comes from the application of identification or learning a model of the system from data. Learning problems trade off the number of a priori assumptions that one must make about a system, as well as the richness of available data, with the complexity of a model that one is able to confidently learn from measured observations. This work offers insight into these tradeoffs by characterizing them precisely over entire spectrums of grey box models of increasing complexity. A third motivation comes from the application of vulnerability analysis, which is the study of sensitivities of system behavior to structural perturbations in a grey-box model describing the attack surface, or representation of the system as visible to a potential attacker. The main results of this work, and its specific contributions, are as follows: 1. We define new graph-theoretic constructs and use them to create a unified framework for structural abstractions, 2. We demonstrate that there will always exist a complete, structure preserving, acyclic abstraction for every single-input, fully-connected system, 3. We define structural controllability of an abstraction of a system and argue why our definition is good, and 4. We show how complete abstractions preserve structural controllability. These results were accepted for publication in two papers at the 2020 International Federation of Automatic Control World Congress, each submitted to a different special invited session. These papers comprise Chapters 2 and 3, respectively, of the thesis presented here, and they are expected to appear in print July 2020.

MESHWR / Department of Hydrology and Water Resources / See the attached abstract below

This document outlines the development of a Design Log Instrument (DLI) intended for use in identifying moments of abstraction as evidence of STEM content knowledge transfer. Many theoretical approaches to explaining knowledge transfer are rooted in a belief that transfer occurs through knowledge abstraction (Reed, Ernst, & Banerji, 1974; Gick & Holyoak, 1980, 1983). The DLI prompts participants to be reflective during technological/engineering design activities. During the development of this instrument, a three-phase multiple case: embedded design was used. Three distinct Phases accommodated the collection and analysis of data necessary for this investigation: Phase 1: Pilot Case Study, Phase 2: Establishing Content Validity, and Phase 3: Establishing Construct Validity. During Phase 3, data from the DLI was collected at each of seven work sessions from two design teams each working through different engineering problems. At the end of Phase 3, a comparison of abstractions found in DLI responses and observation data (Audio/Video transcripts) indicated the extent to which the DLI independently reflected those abstractions revealed in observations (Audio/Video transcripts). Results of this comparison showed that the DLI has the potential to be 68% reliable to reveal abstracted knowledge. Further analysis of these findings showed ancillary correlations between the percent abstractions found per DLI reflective prompt and the percent abstractions found per T/E design phase. Specifically, DLI Reflective Prompts 2 and 3 correlate with T/E Design Phases 3 and 4 (58% and 76% respectively of the total abstractions) which deal with design issues related to investigating the problem and developing alternate solutions. DLI Reflective Prompts 4 and 5 correlate with T/E Design Phases 5 and 6 (22% and 24% respectively of total abstractions) which deal with design issues related to choosing a solution and developing a prototype. Findings also indicate that there are highs and lows of abstraction throughout the T/E design process. The implications of these highs and lows are that specific phases of the T/E design process can be targeted for research and instruction. By targeting specific T/E design phases, a researcher or instructor can increase the likelihood of fostering abstractions as evidence of STEM content knowledge transfer. / Ph. D.

No description available.

Les processus décisionnels de Markov (MDP) sont un formalisme mathématique des domaines de l'intelligence artificielle telle que la planification, l'apprentissage automatique, l'apprentissage par renforcement... Résoudre un MDP permet d'identifier la stratégie (politique) optimale d'un agent en interaction avec un environnement stochastique. Lorsque la taille de ce système est très grande il devient difficile de résoudre ces processus par les moyens classiques. Cette thèse porte sur la résolution des MDP de grande taille. Elle étudie certaines méthodes de résolutions: comme les abstractions et les méthodes dites de projection. Elle montre les limites de certaines abstractions et identifie certaines structures "les bisimulations" qui peuvent s'avérer intéressantes pour une résolution approchée du problème. Cette thèse s'est également intéressée à une méthode de projection l'algorithme Least square temporal difference LSTD(λ). Une estimation de la borne sur la vitesse de convergence de cet algorithme a été établie avec une mise en valeur du rôle joué par le paramètre [lambda]. Cette analyse a été étendue pour déduire une borne de performance pour l'algorithme Least square non stationary policy iteration LS(λ)NSPI en estimant la borne d'erreur entre la valeur calculée à une itération fixée et la valeur sous la politique optimale qu'on cherche à identifier / Markov Decision Processes (MDP) are a mathematical formalism of many domains of artifical intelligence such as planning, machine learning, reinforcement learning... Solving an MDP means finding the optimal strategy or policy of an agent interacting in a stochastic environment. When the size of this system becomes very large it becomes hard to solve this problem with classical methods. This thesis deals with the resolution of MDPs with large state space. It studies some resolution methods such as: abstractions and the projection methods. It shows the limits of some approachs and identifies some structures that may be interesting for the MDP resolution. This thesis focuses also on projection methods, the Least square temporal difference algorithm LSTD(λ). An estimate of the rate of the convergence of this algorithm has been derived with an emphasis on the role played by the parameter [lambda]. This analysis has then been generalized to the case of Least square non stationary policy iteration LS(λ)NSPI . We compute a performance bound for LS([lambda])NSPI by bounding the error between the value computed given a fixed iteration and the value computed under the optimal policy, that we aim to determine

L'animation expressive permet des styles de mouvements exagerés et artistiques comme l'étirement de parties du corps ou encore l'animation de créatures imaginaires comme un dragon. Créer ce genre d'animation nécessite des outils assez flexible afin de déformer les personnages en des poses quelconques, ainsi que de pouvoir contrôler l'animation à tout moment dans le temps. L'approche acutelle pour l'animation expressive est le keyframing: une approche manuelle avec laquelle les animateurs déforment leur personnage un moment spécifique dans le temps en cliquand et glissant la souris sur une partis spécifique du corps---un à la fois. Malgré le fait que cette approche soit flexible, il est difficile de créer des animations de qualité qui suivent les principes artistiques, puisque le keyframing permet seulement qu'un contrôle local spatiallement et temporellement. Lorsqu'ils dessinent des poses ou des mouvements, les artistes s'appuient sur différentes abstractions sous forme de croquis qui facillitent la réalisation de certain principes artistiques. Par example, certains animateurs dessinent des lignes d'action afin de créer une pose plus lisible et expressive. Afin de coordonner un mouvement, les animateurs vont souvent dessiner des abstractions de mouvement comme des demi-cercles pour des sauts, ou des boucles pour des pirouettes---leur permettant de pratiquer la coordination du mouvement. Malheureusement, ces outils artistiques ne font pas partis de l'ensemble d'outils de keyframing actuelle. Le fait que l'on ne puisse pas employer les même outils artistiques pour animater des personnages 3D a une forte conséquence: les outils d'animation 3D ne sont pas employés dans le processus créatif. Aujourd'hui, les animateurs créent sur du papier et utilisent le keyframing seulement à la fin pour réaliser leur animation. La raison pour laquelle nous n'avons pas ces outils artistiques (ligne d'action, abstractions de mouvement) en animation 3D, est parce qu'il manque une compréhension formelle de ceux-ci qui nous permettrais d'exprimer la forme du personnage---potentiellement au cours du temps---en fonction de la forme de ces croquis. Ainsi la contribution principale de cette thèse est une compréhension formelle et mathématique des abstractions de forme et de mouvement courrament employées par des artistes, ainsi qu'un ensemble d'algorithme qui permet l'utilisation de ces outils artistiques pour créer des animations expressives. C'est-à-dire que les outils développés dans cette thèse permettent d'étirer des parties du corps ainsi que d'animer des personnages de différentes morphologies. J'introduis aussi plusieurs extentions à ces outils. Par example, j'explore l'idée de sculpter du mouvement en permettant à l'artiste de dessigner plusieurs couches de mouvement une par dessus l'autre, de twister en 3D les croquis, ou encore d'animer un croquis ligne comme un élastique. Les contributions principales de cette thèse, aussi résumé ci-dessous: -La ligne d'action facilitant la création de poses expressives en dessinant directement le flow complet du personnage. -La courbe spatio-temporelle qui permet de spécifier un mouvement coordoné complet avec un seul geste (en dessinant une seule courbe), applicable à n'importe quel personnage 3D. -Un algorithme de matching rapide et robuste qui permet du ``squash and stretch''. -La ligne d'action élastique avec des attachements dynamiques à la ligne permettant d'animer un personnages à plusieurs jambes (bras) avec une seule ligne 2D animée. / Free-form animation allows for exaggerated and artistic styles of motions such as stretching character limbs and animating imaginary creatures such as dragons. Creating these animations requires tools flexible enough to shape characters into arbitrary poses, and control motion at any instant in time. The current approach to free-form animation is keyframing: a manual task in which animators deform characters at individual instants in time by clicking-and-dragging individual body parts one at a time. While this approach is flexible, it is challenging to create quality animations that follow high-level artistic principles---as keyframing tools only provide localized control both spatially and temporally. When drawing poses and motions, artists rely on different sketch-based abstractions that help fulfill high-level aesthetic and artistic principles. For instance, animators will draw textit{lines of action} to create more readable and textit{expressive} poses. To coordinate movements, animators will sketch textit{motion abstractions} such as semi-circles and loops to coordinate a bouncing and rolling motions. Unfortunately, these drawing tools are not part of the free-form animation tool set today. The fact that we cannot use the same artistic tools for drawing when animating 3D characters has an important consequence: 3D animation tools are not involved in the creative process. Instead, animators create by first drawing on paper, and only later are 3D animation tools used to fulfill the pose or animation. The reason we do not have these artistic tools (the line of action, and motion abstractions) in the current animation tool set is because we lack a formal understanding relating the character's shape---possible over time---to the drawn abstraction's shape. Hence the main contribution of this thesis is a formal understanding of pose and motion abstractions (line of action and motion abstractions) together with a set of algorithms that allow using these tools in a free-form setting. As a result, the techniques described in this thesis allow exaggerated poses and movements that may include squash and stretch, and can be used with various character morphologies. These pose and animation drafting tools can be extended. For instance, an animator can sketch and compose different layers of motion on top of one another, add twist around strokes, or turning the strokes into elastic ribbons. The main contributions of this thesis are summarized as follows: -The line of action facilitating expressive posing by directly sketching the overall flow of the character's pose. -The space-time curve allowing to draft full coordinated movements with a single stroke---applicable to arbitrary characters. -A fast and robust skeletal line matching algorithm that supports squash-and-stretch. -Elastic lines of action with dynamically constrained bones for driving the motion of a multi-legged character with a single moving 2D line.