Cette thèse aborde le problème de navigation d'un système robotique en environnement dynamique et incertain. Plus particulièrement, elle s'intéresse à la détermination du mouvement pour un robot, permettant de rejoindre une position donnée tout en assurant sa propre sécurité et celle des différents agents qui l'entourent. Entre approches délibératives - consistant à déterminer à priori un mouvement complet vers le but - et approches réactives - calculant au cours de la navigation un mouvement à suivre à chaque instant - ont émergé les approches de déformation de mouvement, combinant à la fois une planification de mouvement globale avec un évitement d'obstacles réactif local. Leur principe est simple : un chemin complet jusqu'au but est calculé à priori et fourni au système robotique. Au cours de l'exécution, la partie du mouvement restant être exécutée est déformée continuellement en réponse aux informations sur l'environnement récupérées par les capteurs. Le système peut ainsi modifier son parcours en fonction du déplacement d'obstacles ou de l'imprécision et l'incomplétude de sa connaissance de l'environnement. La plupart des approches de déformations existantes se contentaient de modifier uniquement le chemin géométrique suivi par le robot. Nous proposons alors d'étendre les travaux précédents à une déformation de trajectoire modifiant le mouvement suivi à la fois dans l'espace et dans le temps. Pour ce faire, nous proposons de raisonner sur le futur en utilisant une estimation du comportement futur des obstacles mobiles. En éloignant la trajectoire suivie par le robot du modèle prévisionnel du comportement des obstacles, il est ainsi possible d'anticiper leur mouvement. La trajectoire déformée étant modifiée arbitrairement dans l'espace et dans le temps, l'une des principales difficultés de cette approche consiste à maintenir le respect des contraintes sur le mouvement du robot le long de cette trajectoire et sa convergence vers le but. Une approche de génération de trajectoire avec contrainte sur le temps final a été développée dans ce but. En discrétisant la trajectoire déformée en une séquence d'états-temps successifs, le générateur de trajectoires permet de vérifier si un mouvement faisable existe entre chaque triplé d'états-temps de la trajectoire déformée, et dans le cas contraire de la modifier localement afin de restaurer sa faisabilité. Les approches de déformation et de génération de trajectoire proposées ont été illustrées en simulation puis quelques expérimentations ont été réalisées sur une chaise roulante automatisée.

Les techniques de mesure de diagramme de rayonnement d’antenne actuelles partagent un paradigme commun qui stipule que l’information utile est exclusivement portée par le signal de test généré. Cela implique un effort mécanique fastidieux en faisant tourner l'antenne sous test ou en déplaçant le système de sondes afin de couvrir des angles de mesure différents jusqu'à ce qu'une caractérisation complète soit effectuée ; une limitation qui est généralement surmontée en utilisant des systèmes multisondes coûteux. En outre, toute réflexion provenant du site de mesure et des équipements de test est considérée comme parasite perturbant le signal de test et est ainsi minimisée.Dans cette thèse, un concept de mesure du diagramme de rayonnement d'antenne remettant en cause ce paradigme commun est présenté comme un moyen d'accélérer le processus de caractérisation en utilisant des systèmes économiques. Le paradigme proposé consiste en la génération d'un ensemble d'échos contrôlées, en utilisant des configurations impliquant des plaques réfléchissantes, qui contribueraient directement à la mesure en couvrant différents angles, et récupérer les informations portées par l'ensemble des signaux générés simultanément. Une diversité fréquentielle est introduite afin de générer un système d'équations équilibré où le vecteur inconnu contenant les valeurs du diagramme de rayonnement est récupéré en inversant un problème matriciel. Par conséquent, une attention considérable est accordée au conditionnement du modèle mathématique afin d'assurer la stabilité et la robustesse du systèmeTrois configurations de différents niveaux de complexité en termes d'échos contrôlés sont étudiées, en mettant l'accent sur la configuration la plus simple impliquant un seul écho contrôlé. Des modèles ont été mis au point, avec des contraintes de conception des configurations proposées en termes de dimensionnement et de bandes passante de fonctionnement, mettant en évidence la viabilité mathématique du concept. Les aspects pratiques ont également été évalués en étudiant la tolérance des modèles développés vis-à-vis des erreurs systématiques, ainsi qu’à l'impact de l’application d'un ensemble d’hypothèses simplificatrices. La faisabilité du concept ainsi que son utilité pour accélérer le processus de caractérisation par rapport aux techniques classiques ont été mises en évidence par des simulations numériques. Ce travail ouvre la porte à l'exploitation des échos, généralement considérés comme perturbateurs, dans un contexte de mesure d’antennes. / Current antenna radiation pattern measurement techniques share a common paradigm which states that useful information is exclusively carried by the generated test signal. This implies an excessive, time consuming, mechanical effort by rotating the antenna under test or displacing the probe system in order to cover different measurement angles until a complete scan is performed; a limitation that is typically overcome using costly multi-probe systems. Moreover, any reflection from the measurement site and test equipment is considered spurious as it perturbs the test signal and thus is minimized.In this thesis, an antenna radiation pattern measurement concept challenging this common paradigm is introduced as a mean of accelerating the characterization process using cost-efficient systems. The proposed paradigm consists in the generation of a set of controlled echoes, using set-ups involving highly-reflective plates, which would directly contribute to the measurement alongside the line-of-sight signal by covering different measurement angles, and retrieving the ARP information carried by the set of all generated signals concurrently. Frequency diversity is used in order to generate a balanced system of equations where the unknown ARP vector is retrieved by inverting a matrix problem. Consequently, a considerable attention is paid into the conditioning of the mathematical model in order to ensure the system stability and accuracy.Three configurations of different complexity levels in terms of controlled echoes are studied, with focus on the simplest configuration involving a single controlled echo. Models have been developed with design guidelines for the proposed configurations in terms of set-up dimensions and operating frequency bandwidth highlighting the mathematical viability of the concept. Practical issues were also assessed by studying the tolerance of developed models to systematic practical errors, as well as to the impact of an applied set of simplifying assumptions. The feasibility of the concept as well as its usefulness in accelerating the measurement process with respect to classical techniques were highlighted via numerical simulations. This thesis opens the door for exploiting echoes, generally regarded as a nuisance, in an antenna measurements context.

Les systèmes multi-agents (SMA) peuvent être utilisé pour modéliser les phénomènes qui peuvent être décomposés en plusieurs agents qui interagissent et qui existent au sein d'un environnement. En particulier, ils peuvent être utilisés pour modéliser les sociétés humaines et animales, aux fins de l'analyse de leurs propriétés par des moyens de calcul. Cette thèse est consacrée à l'analyse automatisée d'un type particulier de ces modèles sociaux, à savoir, celles qui sont fondées sur les principes comportementalistes, qui contrastent avec les approches cognitives plus dominante dans la littérature des SMAs. La caractéristique des théories comportementalistes est l'accent mis sur la définition des comportements basée sur l'interaction entre les agents et leur environnement. De cette manière, non seulement des actions réflexives, mais aussi d'apprentissage, les motivations, et les émotions peuvent être définies. Plus précisément, dans cette thèse, nous introduisons une architecture formelle d'agent (spécifiée avec la Notation Z) basée sur la théorie d'analyse comportementale de B. F. Skinner, ainsi que une notion appropriée et formelle de l'environnement (basée sur l'algèbre de processus pi-calculus) pour mettre ces agents ensemble dans un SMA. La simulation est souvent utilisée pour analyser les SMAs. Les techniques consistent généralement à simuler le SMA plusieurs fois, soit pour recueillir des statistiques, soit pour voir ce qui se passe à travers l'animation. Toutefois, les simulations peuvent être utilisés d'une manière plus orientée vers la vérification si on considère qu'elles sont en réalité des explorations de grandes espaces d'états. Dans cette thèse nous proposons une technique de vérification nouvelle basé sur cette idée, qui consiste à simuler un SMA de manière guidée, afin de vérifier si quelques hypothèses sur lui sont confirmées ou non. À cette fin, nous tirons profit de la position privilégiée que les environnements sont dans les SMAs de cette thèse: la spécification formelle de l'environnement d'un SMA sert à calculer les évolutions possibles du SMA comme un système de transition, établissant ainsi l'espace d'états à vérifier. Dans ce calcul, les agents sont pris en compte en les simulant afin de déterminer, à chaque état de l'environnement, quelles sont leurs actions. Chaque exécution de la simulation est une séquence d'états dans cet espace d'états, qui est calculée à la volée, au fur et à mesure que la simulation progresse. L'hypothèse à étudier, à son tour, est donnée comme un autre système de transition, appelé objectif de simulation, qui définit les simulations désirables et indésirables (e.g., "chaque fois que l'agent fait X, il fera Y plus tard"). Il est alors possible de vérifier si le SMA est conforme à l'objectif de simulation selon un certain nombre de notions de satisfiabilité très précises. Algorithmiquement, cela correspond à la construction d'un produit synchrone de ces deux systèmes de transitions (i.e., celui du SMA et l'objectif de simulation) à la volée et à l'utiliser pour faire fonctionner un simulateur. C'est-à-dire, l'objectif de simulation est utilisé pour guider le simulateur, de sorte que seuls les états concernés sont en réalité simulés. À la fin d'un tel algorithme, il délivre un verdict concluant ou non concluant. Si c'est concluant, il est connu que le SMA est conforme à l'objectif de simulation par rapport aux observations qui ont été faites lors des simulations. Si c'est non-concluant, il est possible d'effectuer quelques ajustements et essayer à nouveau. En résumé, donc, dans cette thèse nous fournissons quatre nouveaux éléments: (i) une architecture d'agent; (ii) une spécification formelle de l'environnement de ces agents, afin qu'ils puissent être composés comme un SMA; (iii) une structure pour décrire les propriétés d'intérêt, que nous avons nommée objectif de simulation, et (iv) une technique pour l'analyse formelle du SMA résultant par rapport à un objectif de simulation. Ces éléments sont mis en œuvre dans un outil, appelé Simulateur Formellement Guidé (FGS, de l'anglais Formally Guided Simulator). Des études de cas exécutables dans FGS sont fournies pour illustrer l'approche.

Le passage de l’oralité à l’écrit et de l’indifférence à l’égard des outils de communication de savoir à leur intégration dans un projet éducatif a pris des siècles et il est passé par plusieurs épisodes. Malgré les différences qu’on peut constater quant aux rythmes et aux modalités de cette transformation pédagogique et communicationnelle entre l’Europe et le monde arabe, cette évolution de la réflexion sur les outils et médias éducatifs a fortement influencé la façon avec laquelle ces populations appréhendent aujourd’hui ces techniques de plus en plus numériques. En France, depuis des décennies, les plans numériques pour l’éducation se succèdent. En Tunisie, après la création en 2002 de l’université virtuelle de Tunis (UVT), on parle actuellement de l’intégration de tablettes numériques dans l’école publique. En dépit des différences que présentent ces deux pays quant aux contextes politiques, économiques, sociaux et culturels, nous avons noté des similitudes stratégiques qui caractérisent leurs démarches respectives pour le numérique éducatif. Nous pouvons remarquer, entre autres, une similitude dans l’installation volontariste des techniques pour apprendre accompagnée de discours annonçant plus de facilités, plus de fiabilité et plus de réussite. Dans le cadre de notre recherche, nous nous intéressons à la question de l’enseignement-apprentissage à distance, et aux outils éducatifs mis en œuvre pour ce faire. Nous ne prétendons pas faire une comparaison binaire entre un modèle d’utilisation des technologies dans le cadre de l’apprentissage qui serait français et un autre qui serait tunisien. Nous mettons en revanche en perspectives les deux expériences tout en insistant sur la démarche tunisienne. L’enseignement/apprentissage à distance est une situation de communication particulièrement délicate, d’une part par son inscription dans cette logique de contextes sociaux et économiques, mais aussi par l’éclatement de la notion de l’espace qui renforce le sentiment de l’isolement chez l’apprenant. Pour surmonter ce sentiment d’isolement et réussir son apprentissage à distance, plusieurs chercheurs proposent un processus d’autorégulation de l’apprentissage. Bien qu’il soit centré sur l’activité de l’apprenant lui-même, ce processus insiste sur l’importance de l’intervention des autres usagers du système éducatif (institution et corps pédagogique). Par notre recherche, nous avons voulu interroger cette question d’autorégulation de l’apprentissage dans le contexte tunisien de l’université virtuelle de Tunis. Nous avons alors cherché à comprendre le comportement autorégulé des apprenants tunisiens à la lumière du dispositif (humain et technique) de l’institution. Pour soulever ces questions nous avons opté pour une méthodologie multiple qui réunit observation participante, observation cachée, questionnaire, protocole géode et analyse de contenu. Cette recherche a abouti à trois résultats majeurs : la création de l’UVT est un projet avant tout politique destiné à véhiculer une image moderne de la Tunisie. En effet, à part l’expérience de l’institut supérieur de la formation continue crée en 1984, aucune réflexion autour d’une pédagogie adaptée à l’enseignement-apprentissage à distance dans le terrain tunisien n’a été entamée surtout que le dispositif UVT est basé sur les technologies numériques. De ce fait, le comportement autorégulé des apprenants oscille, selon le degré de contrôle pédagogique qu’exerce le dispositif UVT sur leur apprentissage, entre adaptation aux conditions formelles et création de conditions informelles contournant ainsi le dispositif de l’institution. / The transition from spoken (unwritten, said, told) to written and from the meaninglessness towards the communication tools and then to their integration in an educational project has taken centuries and has gone through several chapters. Despite the differences that can be perceived on the rhythms and modalities of this educational and communicational transformation between Europe and the Arab world, this evolution of thinking about educational tools and media has greatly influenced the way people apprehend these techniques. Especially considering that these techniques are more and more digital today. In France, for decades, several digital plans for education have been implemented. In Tunisia, after the creation of the Virtual University of Tunis in 2002, a project about the integration of digital tablets in public schools had been announced. Despite the political, economic, social and cultural differences between these two countries, we noticed strategic similarities that characterize their respective digital educational approaches. We can note, among others, a similarity in the voluntary installation of educational techniques accompanied by speeches announcing easiness, more reliability and more success. In the framework of our research, we focus on the issue of e-learning and the tools implemented for it. We are not doing a binary comparison between the way that technology in education is used in France and the way that technology in education is used in Tunisia. We, however, prospect both experiences while emphasizing the Tunisian approach. E-learning is a particularly delicate communication situation, not only because it is influenced by social and economic factors, but also because of the bursting of the notion of space that exasperate the learners’ feeling of isolation. To overcome this feeling of isolation and for successful distance learning, several researchers propose a self-regulation process. While it is centered on the activity of the learner himself, this process insists on the importance of the intervention of all education system users. Through our research, we wanted to ask the question of self-regulated learning in the Tunisian context represented by the Virtual University of Tunis (VUT). We then sought to understand the self-regulated behavior of Tunisian students (learners) in the light of the institute system. To raise these issues we opted for a methodology that combines observation, questionnaire, geode protocol and content analysis. This research led to three major outcomes: the creation of the VUT is a political project intended to convey a modern image of Tunisia. Indeed, besides the experience of the Higher Institute of Continuing Education, established in 1984, no reflection on a pedagogy adapted to distance learning in Tunisia has been implemented especially that the VUT is based on digital technologies. Thus, the self-regulated learner behavior varies, according to the degree of control exerted by the VUT environment on their learning activities, between adaptation to the formal requirements and creating informal conditions.

Nos travaux s’inscrivent dans le cadre de la formation à la gestion de crise en environnements virtuels. La scénarisation joue un rôle essentiel pour l’apprentissage humain en environnement virtuel. Cela permet à la fois de proposer et d’orchestrer des situations d’apprentissage personnalisées et également d’amener l’apprenant vers des scénarios pertinents et formateurs. Les travaux présentés dans cette thèse s’intéressent à la génération dynamique de scénarios et à leur exécution en environnements virtuels. Pour cette scénarisation, nous visons un ensemble d’objectifs qui sont souvent contradictoires : la liberté d’action de l’utilisateur, la génération de scénarios variés et fidèles à l’intention de l’auteur, le contrôle scénaristique et la résilience du système de scénarisation. Les différentes approches de la narration interactive favorisent plus ou moins certains de ces objectifs mais il est difficile de tous les concilier, et c’est là l’enjeu de nos travaux. En plus de ces objectifs, nous cherchons également à faciliter la modélisation du contenu scénaristique qui est encore de nos jours un réel enjeu lorsqu’il s’agit de scénariser des environnements complexes comme celui de la gestion de crise. Nous proposons une approche émergente dont le scénario vécu par l’apprenant va émerger des interactions entre l’apprenant, les personnages virtuels et notre système de scénarisation MENTA. MENTA est chargé du contrôle scénaristique en proposant un ensemble d’ajustements (sur la simulation) répondant à des objectifs scénaristiques choisis par le formateur (p. ex., faire travailler certaines compétences en particulier). Ces ajustements prennent la forme d’un scénario prescrit qui est généré par MENTA via un moteur de planification que nous avons couplé avec des cartes cognitives floues au travers d’un macro-opérateur FRAG. Un FRAG permet de modéliser des fragments de scénarios sous la forme de séquence d’actions/événements scriptés. L’originalité de notre approche repose sur un couplage fort entre planification et modèles graphiques qui permet de conserver les propriétés d’exploration et de puissance générative d’un moteur de planification (ce qui favorise la variabilité et la résilience du système), tout en facilitant la modélisation du contenu scénaristique ainsi que l’intention de l’auteur au travers de morceaux de scénario qui vont être scriptés par l’auteur et réutilisés dans la planification. Nous avons travaillé sur un exemple applicatif concret de scénarios portant sur la gestion d’un afflux massif de blessés, puis nous avons implémenté MENTA et généré des scénarios relatifs à cet exemple. Enfin, nous avons testé et analysé les performances de notre système. / Our work is related to the training of crisis management in virtual environments. The specification of possible unfoldings of events in a simulation is essential for human learning in a virtual environment. This allows both to propose and orchestrate personalized learning situations and also to bring the learner toward relevant and educative scenarios. The work presented in this thesis focuses on the dynamic generation of scenarios and their execution in a virtual environment. For that, we aim at a set of objectives that are often contradictory : the freedom of action of the user, the generation of various scenarios that respect the authorial intent, the narrative control and the capacity of the system to adapt to deviations fromthe learner. The different approaches of interactive storytelling tackle more or less some of these objectives, but it is difficult to satisfy them all, and this is the challenge of our work. In addition to these objectives, we also aim at facilitating the modeling of the narrative content, which is still a real issue today when it comes to model complex environments such as the ones related to crisis management. We propose an emergent approachwhere the scenario experienced by the learner will emerge fromthe interactions between the learner, the virtual characters and our narrative system MENTA. MENTA is in charge of the narrative control by proposing a set of adjustments (over the simulation) that satisfies narrative objectives chosen by the trainer (e. g., a list of specific skills). These adjustments take the form of a prescribed scenario that is generated by MENTA via a planning engine that we have coupled with fuzzy cognitive maps through a macro-operator FRAG. A FRAG is used to model FRAGment of scenario in the form of scripted sequences of actions/events. The originality of our approach relies on a strong coupling between planning and graphical models which preserves the exploration capability and the generative power of a planning engine (which contributes to the generation of various and adaptable scenarios), while facilitating the modeling of narrative content as well as the authorial intent thanks to fragments of scenario that are scripted by the author and used during the planning process. We have worked on a concrete application example of scenarios dealing with the management of a massive influx of victims. Then, we have implemented MENTA and generated scenarios related to this example. Finally, we have tested and analyzed the performance of our system.

Les systèmes multi-agents (SMA) peuvent être utilisé pour modéliser les phénomènes qui peuvent être décomposés en agents qui interagissent et qui existent au sein d'un environnement. Ils peuvent être utilisés pour modéliser les sociétés humaines et animales, aux fins de l'analyse de leurs propriétés par des moyens de calcul. Cette thèse est consacrée à l'analyse automatisée d'un type particulier de ces modèles sociaux, celles qui sont fondées sur les principes comportementalistes, qui contrastent avec les approches cognitives plus dominantes dans la littérature des SMAs. La caractéristique des théories comportementalistes est l'accent mis sur la définition des comportements basée sur l'interaction entre les agents et leur environnement. Non seulement des actions réflexives, mais aussi d'apprentissage, les motivations, et les émotions peuvent être définies. Nous introduisons une architecture formelle d'agent basée sur la théorie d'analyse comportementale de B. F. Skinner, ainsi que une notion appropriée et formelle de l'environnement pour mettre ces agents ensemble dans un SMA. La simulation est souvent utilisée pour analyser les SMAs. Les techniques consistent généralement à simuler le SMA plusieurs fois, soit pour recueillir des statistiques, soit pour voir ce qui se passe à travers l'animation. Toutefois, les simulations peuvent être utilisées d'une manière plus orientée vers la vérification si on considère qu'elles sont en réalité des explorations de grandes espaces d'états. Nous proposons une technique de vérification nouvelle basé sur cette idée, qui consiste à simuler un SMA de manière guidée, afin de vérifier si quelques hypothèses sur lui sont confirmées ou non. À cette fin, nous tirons profit de la position privilégiée que les environnements sont dans les SMAs de cette thèse: la spécification formelle de l'environnement d'un SMA sert à calculer les évolutions possibles du SMA comme un système de transition, établissant ainsi l'espace d'états à vérifier. Dans ce calcul, les agents sont pris en compte en les simulant afin de déterminer, à chaque état de l'environnement, quelles sont leurs actions. Chaque exécution de la simulation est une séquence d'états dans cet espace d'états, qui est calculée à la volée, au fur et à mesure que la simulation progresse. L'hypothèse à étudier, à son tour, est donnée comme un autre système de transition, appelé objectif de simulation, qui définit les simulations désirables et indésirables. Il est alors possible de vérifier si le SMA est conforme à l'objectif de simulation selon un certain nombre de notions de satisfiabilité très précises. Algorithmiquement, cela correspond à la construction d'un produit synchrone de ces deux systèmes de transitions (i.e., celui du SMA et l'objectif de simulation) à la volée et à l'utiliser pour faire fonctionner un simulateur. C'est-à-dire, l'objectif de simulation est utilisé pour guider le simulateur, de sorte que seuls les états concernés sont en réalité simulés. À la fin d'un tel algorithme, il délivre un verdict concluant ou non concluant. Si c'est concluant, il est connu que le SMA est conforme à l'objectif de simulation par rapport aux observations qui ont été faites lors des simulations. Si c'est non-concluant, il est possible d'effectuer quelques ajustements et essayer à nouveau. En résumé, dans cette thèse nous fournissons quatre nouveaux éléments: (i) une architecture d'agent; (ii) une spécification formelle de l'environnement de ces agents, afin qu'ils puissent être composés comme un SMA; (iii) une structure pour décrire les propriétés d'intérêt, que nous avons nommée objectif de simulation, et (iv) une technique pour l'analyse formelle du SMA résultant par rapport à un objectif de simulation. Ces éléments sont mis en œuvre dans un outil, appelé Simulateur Formellement Guidé (FGS, de l'anglais Formally Guided Simulator).Des études de cas exécutables dans FGS sont fournies pour illustrer l'approche. / Multi-agent systems (MASs) can be used to model phenomena that can be decomposed into several interacting agents which exist within an environment. In particular, they can be used to model human and animal societies, for the purpose of analysing their properties by computational means. This thesis is concerned with the automated analysis of a particular kind of such social models, namely, those based on behaviourist principles, which contrasts with the more dominant cognitive approaches found in the MAS literature. The hallmark of behaviourist theories is the emphasis on the definition of behaviour in terms of the interaction between agents and their environment. In this manner, not merely reflexive actions, but also learning, drives, and emotions can be defined. More specifically, in this thesis we introduce a formal agent architecture (specified with the Z Notation) based on the Behaviour Analysis theory of B. F. Skinner, and provide a suitable formal notion of environment (based on the pi-calculus process algebra) to bring such agents together as a MAS. Simulation is often used to analyse MASs. The techniques involved typically consist in implementing and then simulating a MAS several times to either collect statistics or see what happens through animation. However, simulations can be used in a more verification-oriented manner if one considers that they are actually explorations of large state-spaces. In this thesis we propose a novel verification technique based on this insight, which consists in simulating a MAS in a guided way in order to check whether some hypothesis about it holds or not. To this end, we leverage the prominent position that environments have in the MASs of this thesis: the formal specification of the environment of a MAS serves to compute the possible evolutions of the MAS as a transition system, thereby establishing the state-space to be investigated. In this computation, agents are taken into account by being simulated in order to determine, at each environmental state, what their actions are. Each simulation execution is a sequence of states in this state-space, which is computed on-the-fly, as the simulation progresses. The hypothesis to be investigated, in turn, is given as another transition system, called a simulation purpose, which defines the desirable and undesirable simulations (e.g., "every time the agent does X, it will do Y later"). It is then possible to check whether the MAS satisfies the simulation purpose according to a number of precisely defined notions of satisfiability. Algorithmically, this corresponds to building a synchronous product of these two transitions systems (i.e., the MAS's and the simulation purpose) on-the-fly and using it to operate a simulator. That is to say, the simulation purpose is used to guide the simulator, so that only the relevant states are actually simulated. By the end of such an algorithm, it delivers either a conclusive or inconclusive verdict. If conclusive, it becomes known whether the MAS satisfies the simulation purpose w.r.t. the observations made during simulations. If inconclusive, it is possible to perform some adjustments and try again.In summary, then, in this thesis we provide four novel elements: (i) an agent architecture; (ii) a formal specification of the environment of these agents, so that they can be composed into a MAS; (iii) a structure to describe the property of interest, which we named simulation purpose; and (iv) a technique to formally analyse the resulting MAS with respect to a simulation purpose. These elements are implemented in a tool, called Formally Guided Simulator (FGS). Case studies executable in FGS are provided to illustrate the approach.

Depuis quelques années, des recherches décrivent des effets alarmants de l’exposition à des environnements acoustiques artificiels sur les propriétés fonctionnelles des neurones du système auditif. L’objectif de ce projet était de déterminer si une exposition à très long terme à une intensité sonore, qui n’est pas reconnue par les législations pour provoquer des pertes permanentes ou temporaires (80dB SLP 8h/jour), induisait ou pas des changements au niveau des audiogrammes et des propriétés fonctionnelles des neurones du cortex auditif primaire.Des rattes adultes (Sprague Dawley) ont été exposées entre 3 mois à 18 mois (selon les groupes) à un milieu acoustique mimant les environnements sonores quotidiens de la majorité de la population et dont les effets n’ont jamais été étudiés sur de telles durées. L’originalité de ce projet réside dans l’analyse des effets à tous les niveaux du système auditif depuis le niveau périphérique (ABRs) jusqu’au niveau central (électrophysiologie corticale) ainsi que les conséquences possibles au niveau comportemental. Une tâche d’apprentissage perceptif inédite a été mise au point afin d’évaluer les effets de l’exposition. Au cours du vieillissement, nos données montrent une baisse des performances comportementales, une atteinte progressive des seuils ABRs et des atteintes de certains paramètres des réponses neuronales comme (i) la latence, (ii) la durée, (iii) la détection de silence dans une vocalisation, (iv) le suivit d’une modulation d’amplitude, (v) la reproductibilité des réponses à une vocalisation. Le principal effet de l’exposition à un environnement bruité est l’apparition d’un TTS après 6 à 12 mois d’exposition (qui disparait complètement en 3 semaines), sans que cela ait, de façon très surprenante, la moindre conséquence notable sur les seuils ABRs, l’activité évoquée corticale, ou les performances de discrimination des animaux. Ces résultats nous incitent à la prudence sur la généralisation des conclusions à tirer des expositions à des environnements bruités artificiels. / Over the last few years, studies have described alarming effects of exposure to artificial acoustic environments on the functional properties of neurons in the auditory system. The aim of this project was to determine if long-lasting exposure at a sound intensity which is not recognized by the legislation to cause permanent or temporary hearing loss (80 dB SLP 8h/ day) induced, or not, changes in the audiograms and functional properties of neurons in theprimary auditory cortex. Adult female rats (Sprague Dawley) were exposed over 3 to 18 months (depending on the group) to an acoustic environment mimicking daily sound environments surrounding a large part of the population, and whose effects have never been studied on such durations. The originality of this project lies in analyzing the effects at alllevels of the auditory system from peripheral (via ABRs) to central levels (cortical electrophysiology) and also the possible consequences at the behavioral level. A new perceptual learning task has been developed to assess the effects of exposure. During aging, our data showed a decrease in behavioral performance, a gradual impairment of ABRs thresholds as well as an impairment in parameters of the neural responses such as (i) the response latency, (ii) response duration, (iii) the ability to detect silence in a vocalization (iv) or to follow an amplitude modulation, (v) the reproducibility of response to vocalization. The main effect of exposure to a noisy environment is the appearance of a Temporary Threshold Shift (TTS) after 6 to 12 months of exposure (which completely disappears in three weeks). Surprisingly, this long lasting TTS had apparently no e ffect on ABRs thresholds, the evokedcortical activity, or the animal’s discrimination performance. These results encourage us to be quite cautious in generalizing the conclusions to be drawn from exposures to artificial noisyenvironments.

With the continued development towards a digitalized and data-driven world, the importance of visual data analysis is increasing as well. Visual data analysis enables people to interactively explore and reason on certain data through the combined use of multiple visualizations. This is relevant for a wide range of application domains, including personal, professional, and public ones. In parallel, a ubiquity of modern devices with very heterogeneous characteristics has spawned. These devices, such as smartphones, tablets, or digital whiteboards, can enable more flexible workflows during our daily work, for example, while on-the-go, in meetings, or at home. One way to enable flexible workflows is the combination of multiple devices in so-called device ecologies. This thesis investigates how such a combined usage of devices can facilitate the visual data analysis of multivariate data sets. For that, new approaches for both visualization and interaction are presented here, allowing to make full use of the dynamic nature of device ecologies. So far, the literature on these aspects is limited and lacks a broader consideration of data analysis in device ecologies. This doctoral thesis presents investigations into three main parts, each addressing one research question: (i) how visualizations can be adapted for heterogeneous devices, (ii) how device pairings can be used to support data exploration workflows, and (iii) how visual data analysis can be supported in fully dynamic device ecologies. For the first part, an extended analytical investigation of the notion of responsive visualization is contributed. This investigation is then complemented by the introduction of a novel matrix-based visualization approach that incorporates such responsive visualizations as local focus regions. For the two other parts, multiple conceptual frameworks are presented that are innovative combinations of visualization and interaction techniques. In the second part, such work is conducted for two selected display pairings, the extension of smartwatches with display-equipped watchstraps and the contrary combination of smartwatch and large display. For these device ensembles, it is investigated how analysis workflows can be facilitated. Then, in the third part, it is explored how interactive mechanisms can be used for flexibly combining and coordinating devices by utilizing spatial arrangements, as well as how the view distribution process can be supported through automated optimization processes. This thesis’s extensive conceptual work is accompanied by the design of prototypical systems, qualitative evaluations, and reviews of existing literature.