Ce mémoire a pour objectif de préciser le sens du verbe « abêtir » dans les Pensées de Blaise Pascal. Le sort ayant voulu que l’Apologie de la religion chrétienne demeure à jamais inachevée, le philosophe a emporté un secret épineux dans sa tombe : Qu’a-t-il bien pu vouloir signifier en écrivant que le remède à l’incroyance – répéter les gestes et les paroles liés au culte chrétien – abêtit ? Nous montrons à titre préliminaire que s’abêtir signifie devenir-bête, et que ce changement d’état entretient des liens étroits, tant par le contexte de son énonciation que par son champ lexical, avec le « discours de la Machine » et la notion d’« automate ». Notre analyse permet d’inférer que d’un point de vue strictement formel, s’abêtir renvoie à la préparation des habitudes humaines en vue de la foi. Nous montrons dans les chapitres suivants que le vocabulaire de la Machine/automate/bête est susceptible d’éclaircir trois dimensions de cette préparation. En distinguant les perspectives psycho-physiologique, morale et gnoséologique sur le problème de la conversion religieuse, nous montrons que l’abêtissement peut renvoyer simultanément 1) à l’acquisition d’habitudes corporelles et intellectuelles qui conduisent à la foi ; 2) au renforcement de la vertu d’humilité contre l’orgueil hérité du péché originel et qui fait obstacle à la croyance ; 3) et à l’acquisition passive d’une panoplie de connaissances factuelles tirées des Écritures et de l’histoire, nécessaires à une bonne entente des preuves de la vérité du christianisme. Chacune de ces perspectives fait l’objet d’un chapitre. / This Master’s thesis aims to clarify the meaning of “s’abêtir” in Blaise Pascal’s Pensées. As the Apologie de la religion chrétienne was left unfinished, the French philosopher took his secret to the grave: What did he mean by the idea that the cure for unbelief – repeating actions and words related to Christian worship – results in “s’abêtir” ? I argue that “s’abêtir” means becoming-beast, and that the context in which the notion is uttered as well as the lexical field it covers relate to the “discours de la Machine” and the notion of “automate”. My analysis allows me to say that, formally, “s'abêtir” refers to the preparation of human habits to faith. In the following chapters, I show that the vocabulary of Machine/automate/bête is likely to clarify three dimensions for such a preparation. Depending on the position we adopt with respect to the problem of belief, that is, from a psycho-physiological, moral or epistemological perspective, “s’abêtir” can simultaneously mean 1) acquiring corporeal and intellectual habits that lead to faith ; 2) strengthening the virtue of humility against pride, inherited from original sin ; 3) passively acquiring a range of factual knowledge from Scripture and history necessary to understand the evidence of the truth of Christianity. Each one of these perspectives is the topic of one of the successive chapters of this thesis.

La marionnette, petite Marie d’après son étymologie, figure réduite à l’image de l’homme, être diminutif ou condensé, actrice « dramatico-végétale » selon l’écrivain Carlo Collodi, amuse, effraie ou fascine depuis toujours l’être humain. Nous en trouvons des traces dès l’Antiquité en occident. Telle l’automate Olympia dans L’Homme au sable d’Ernst Hoffmann, qui inspira à Freud le concept d’ « Inquiétante étrangeté », la marionnette fait douter le spectateur : celui-ci ressent une étrange impression à la vue d’un objet sans vie qui paraît animé, un malaise comparable à celui qu’il éprouve en voyant une personne se comporter en « Homme-machine » (La Mettrie).Ce travail propose d’explorer l’existence paradoxale des figures inanimées dans le but d’expliquer comment celles-ci semblent prendre vie, mourir ou ressusciter à l’envi. A quel projet artisanal ou fantasme démiurgique répond la fabrication des créatures artificielles ? Comment l’esprit vient aux objets ? Quelles parts occupent le mouvement impulsé par le manipulateur et les croyances et projections du spectateur dans ce mystérieux phénomène d’animation ? Ce travail qui s’inscrit dans le domaine des études théâtrales traverse d’autres champs disciplinaires, notamment la littérature, la psychanalyse, la philosophie, l’anthropologie et l’histoire. / The puppet, or marionnete, - little Marie etymologically –, a human model, in reduction, a diminutive or condensed creature, a « dramatico-vegetable » actor in the eyes of writer Carlo Collodi, has always amused, frightened or fascinated mankind. Traces of puppets are to be found early in western ancient times. In much the same way as the automaton Olympia, in Ernst Hoffmann's The Sand Man, inspired Freud's concept of « disquieting strangeness », (Unheimliche), the puppet creates doubt in the spectator's mind : the latter feels strange when viewing an inanimate object apparently gifted with life, an unease akin to that which one feels if confronted with a human behaving like a ' « Man-machine » (La Mettrie).This work aims at exploring the paradoxical world of inanimate figures in order to explain how those seem to acquire life, lose it or come to life again at will. To what craft project or demiurgic fantasy does the making of artificial creatures answer ? How does the soul come to those objects ? What are the shares of the motions impulsed by the puppet manipulator and the beliefs and projections of the spectators, in that mysterious phenomenon of animation. The present work, although fully belonging to the field of drama studies, crosses others, notably literature, psychoanalysis, philosophy, anthropology and history.

Esta tese apresenta uma proposta de aplicação de formalismos adaptativos na modelagem e elaboração de cursos para softwares educacionais. A princípio, soluções adaptativas podem ser incorporadas a qualquer tipo de dispositivo guiado por regras. Neste projeto, o dispositivo subjacente utilizado será a Máquina de Moore, que é um autômato finito com saída associada aos seus estados. Assim, para cada estado pode-se associar o material didático a ser apresentado pela função de saída. Aplicando-se os conceitos de adaptatividade nesse transdutor, é possível elaborar cursos dinâmicos, que se auto-modifiquem com base em regras definidas pelo professor e pelas experiências e nível de conhecimento individualizado dos alunos. Para complementar o trabalho, é apresentado um protótipo de curso baseado em Máquina de Moore Adaptativa. / This thesis presents a proposal for application of adaptive formalisms for modeling and development of courses for educational software. In principle, adaptive solutions can be incorporated into any type of device guided by rules. In this project, the device will be used behind the Moore Machine, which is a finite automaton with outputs associated with their states. Thus, for each state we can associate the material to be presented by the function output. Applying the concepts of adaptive technology this transducer, you can develop dynamic courses, which are self-modifying based on rules defined by the teacher, and the level of experience and knowledge of individual students. To complement the work is presented a prototype of course based on Adaptive Moore Machine.

Visando representar linhas retas digitais, segmentos digitalizados e arcos, cada uma das linhas de pesquisa disponíveis apresenta suas vantagens e aplicações apropriadas. No entanto, considerando as complexidades de cenários do mundo real, o uso dessas representações não é tão popular em situações que requerem modelos flexíveis ou envolvendo interferências espúrias. As tecnologias adaptativas são formalismos da ciência da computação capazes de alterar seu comportamento dinamicamente, sem a interferência de agentes externos, em resposta a estímulos de entrada. Ao serem capazes de responder às mencionadas condições variáveis do ambiente, os dispositivos adaptativos naturalmente tendem a apresentar a flexibilidade requerida para atuarem em cenários dinâmicos. Assim, este trabalho investiga uma alternativa fundamentada no autômato finito adaptativo por meio do dispositivo denominado segmento digitalizado adaptativo, que incorpore o poder expressivo de representar parâmetros desses segmentos. Dentre esses parâmetros destacam-se a capacidade de representar as tolerâncias, a escalabilidade, os erros causados por desvios em ângulo ou em comprimento dos segmentos mencionados, resultando em estruturas mais flexíveis. Considerando que os métodos sintáticos são estruturais, os segmentos digitalizados adaptativos são modelados por conjuntos de regras, partindo-se de primitivas, concebendo-se as funções adaptativas correspondentes para alteração dos estados e de regras de transição. Posteriormente, estruturas mais elaboradas são concebidas relacionadas a arcos digitais pelos quais cadeias (strings) estimulam, em um passo único, autômatos finitos adaptativos que implementam segmentos digitalizados adaptativos. As implementações utilizam uma ferramenta cujo núcleo é um simulador para edição dos arquivos que compõem os autômatos. Consequentemente, o método proposto torna-se uma alternativa relativamente simples e intuitiva comparando-se com as abordagens existentes, apresentando capacidade de aprendizagem, além de ser computacionalmente poderosa. / For the representation of digital straight lines, digitized straight line segments and arcs, each of the available research approaches has its advantages and suitable applications. However, taking into account the complexities of real-world scenarios, the use of these representations is not so popular in situations that require flexible models or involving spurious interferences. Adaptive technologies are computer science formalisms able to change their behavior dynamically, without the interference of external agents, in response to incoming stimuli. By being able to respond to changing environmental conditions, adaptive devices naturally tend to have the required flexibility to work in dynamic scenarios. Thus, the purpose of this study is to investigate an alternative based on adaptive finite automaton through the device called adaptive digitized straight line segment, incorporating the expressive power to represent parameters of these segments. Among these parameters, emphasis is given to the ability to represent tolerances, scalability or errors caused by deviations in angle or length of the mentioned segments, resulting in more flexible structures. Whereas syntactic methods are structural, adaptive digitized straight line segments are modeled by sets of rules, starting from primitives, conceiving the corresponding adaptive functions to amend the set of states and transition rules. Later, more elaborate structures are designed related to digital arcs the corresponding strings of which stimulate, in just a single step, adaptive finite automata that implement adaptive digitized straight line segments. The implementations use a simulator for editing the files that compose the automata. Consequently, the proposed method reveals to be a simple and intuitive alternative capable of learning, besides being computationally powerful.

Investigações da dinâmica crítica em modelos de magnetismo, para tempos curtos, têm aparecido com grande freqüência na literatura. Essa técnica foi descoberta por Li, Schülke e Zheng que, inspirados em trabalhos anteriores de Huse e Janssen et al., mostraram que generalizações de grandezas como a magnetização e o cumulante de Binder exibem comportamento universal já no início da simulação. O estudo da criticalidade em tempos curtos proporciona um caminho alternativo para a estimativa do expoente z, além de permitir o cálculo de um novo expoente dinâmico θ, associado ao comportamento anômalo da magnetização. Da mesma forma, simulações dependentes do tempo tornaram-se ferramenta útil para estudar transições de fase em autômatos celulares e modelos de spin. Em particular, as melhores estimativas para o expoente z do Ising bidimensional foram obtidas por meio da técnica de propagação de danos, introduzida por Kauffman no estudo de autômatos e mais tarde generalizada para modelos de spin. Na primeira parte deste trabalho utilizamos o método Monte Carlo em tempos curtos para investigar o modelo de Baxter-Wu, definido em uma rede bidimensional triangular com variáveis do tipo Ising, acopladas por interações de três corpos. Obtivemos os expoentes críticos dinâmicos z e θ além dos índices críticos estáticos ß e Nû. Os resultados não corroboram aqueles recentemente obtidos por Santos e Figueiredo para o expoente z. Na segunda parte do trabalho, investigamos a propagação de danos no modelo de Ising unidimensional submetido a duas dinâmicas propostas por Hinrichsen e Domany (HD). Em particular, nós estudamos o efeito da atualização síncrona (paralela) e assíncrona (dinâmica contínua) sobre o espalhamento do dano. Mostramos que o dano não se propaga quando a segunda dinâmica é implementada de forma assíncrona. Também mostramos que as regras para atualização do dano produzidas por essa dinâmica, quando a temperatura vai a infinito e um certo parâmetro Lambda é igual a zero, são equivalentes àquelas do bem conhecido autômato celular (modelo A) de Grassberger. / Short-time simulations have been used with great frequency in the literature. That technique was discovered by Li, Shülke and Zheng that, inspired in previous works by Huse and Janssen et al., showed that generalizations of quantities like magnetization and the Binder´s cumulant exhibit universal behavior in the beginning of the simulation (early time behavior). The study of criticality in short-times provides an alternative way to estimate the dynamic critical exponent z, besides allowing the calculation of a new dynamic exponent θ, associated to the anomalous behavior of the magnetization. In the same way, time-dependent simulations became a useful tool to study phase transitions in cellular automata and also for spin models. In fact, the best estimates for the exponent z of the two-dimensional Ising model were obtained through the technique of damage spreading, introduced by Kauffman in the study of cellular automata, later widespread for spin models. In the first part of this work we used short-time Monte Carlo simulations to investigate the Baxter-Wu model, defined in a triangular lattice whose variables are Ising-like coupled by triplet interactions. We have obtained estimates for the dynamic critical exponents z and θ besides static exponents ß e Nû. Our results do not corroborate recent estimates by Santos and Figueiredo for the critical exponent z. In the second part of this work, we investigated the damage spreading in the one-dimensional Ising model under two dynamics introduced by Hinrichsen and Domany (HD). In particular, we study the effects of synchronous (parallel) and asynchronous (continuous dynamics) updating on the spreading properties. We showed that the damage does not spread when the second dynamic is implemented in an asynchronous way. We found that the rules for updating the damage produced by this dynamic, as the temperature goes to infinity and a certain parameter Lambda is zero, are equivalent to those of Grassberger’s well-known model A cellular automaton.

Visando representar linhas retas digitais, segmentos digitalizados e arcos, cada uma das linhas de pesquisa disponíveis apresenta suas vantagens e aplicações apropriadas. No entanto, considerando as complexidades de cenários do mundo real, o uso dessas representações não é tão popular em situações que requerem modelos flexíveis ou envolvendo interferências espúrias. As tecnologias adaptativas são formalismos da ciência da computação capazes de alterar seu comportamento dinamicamente, sem a interferência de agentes externos, em resposta a estímulos de entrada. Ao serem capazes de responder às mencionadas condições variáveis do ambiente, os dispositivos adaptativos naturalmente tendem a apresentar a flexibilidade requerida para atuarem em cenários dinâmicos. Assim, este trabalho investiga uma alternativa fundamentada no autômato finito adaptativo por meio do dispositivo denominado segmento digitalizado adaptativo, que incorpore o poder expressivo de representar parâmetros desses segmentos. Dentre esses parâmetros destacam-se a capacidade de representar as tolerâncias, a escalabilidade, os erros causados por desvios em ângulo ou em comprimento dos segmentos mencionados, resultando em estruturas mais flexíveis. Considerando que os métodos sintáticos são estruturais, os segmentos digitalizados adaptativos são modelados por conjuntos de regras, partindo-se de primitivas, concebendo-se as funções adaptativas correspondentes para alteração dos estados e de regras de transição. Posteriormente, estruturas mais elaboradas são concebidas relacionadas a arcos digitais pelos quais cadeias (strings) estimulam, em um passo único, autômatos finitos adaptativos que implementam segmentos digitalizados adaptativos. As implementações utilizam uma ferramenta cujo núcleo é um simulador para edição dos arquivos que compõem os autômatos. Consequentemente, o método proposto torna-se uma alternativa relativamente simples e intuitiva comparando-se com as abordagens existentes, apresentando capacidade de aprendizagem, além de ser computacionalmente poderosa. / For the representation of digital straight lines, digitized straight line segments and arcs, each of the available research approaches has its advantages and suitable applications. However, taking into account the complexities of real-world scenarios, the use of these representations is not so popular in situations that require flexible models or involving spurious interferences. Adaptive technologies are computer science formalisms able to change their behavior dynamically, without the interference of external agents, in response to incoming stimuli. By being able to respond to changing environmental conditions, adaptive devices naturally tend to have the required flexibility to work in dynamic scenarios. Thus, the purpose of this study is to investigate an alternative based on adaptive finite automaton through the device called adaptive digitized straight line segment, incorporating the expressive power to represent parameters of these segments. Among these parameters, emphasis is given to the ability to represent tolerances, scalability or errors caused by deviations in angle or length of the mentioned segments, resulting in more flexible structures. Whereas syntactic methods are structural, adaptive digitized straight line segments are modeled by sets of rules, starting from primitives, conceiving the corresponding adaptive functions to amend the set of states and transition rules. Later, more elaborate structures are designed related to digital arcs the corresponding strings of which stimulate, in just a single step, adaptive finite automata that implement adaptive digitized straight line segments. The implementations use a simulator for editing the files that compose the automata. Consequently, the proposed method reveals to be a simple and intuitive alternative capable of learning, besides being computationally powerful.

Esta tese apresenta uma proposta de aplicação de formalismos adaptativos na modelagem e elaboração de cursos para softwares educacionais. A princípio, soluções adaptativas podem ser incorporadas a qualquer tipo de dispositivo guiado por regras. Neste projeto, o dispositivo subjacente utilizado será a Máquina de Moore, que é um autômato finito com saída associada aos seus estados. Assim, para cada estado pode-se associar o material didático a ser apresentado pela função de saída. Aplicando-se os conceitos de adaptatividade nesse transdutor, é possível elaborar cursos dinâmicos, que se auto-modifiquem com base em regras definidas pelo professor e pelas experiências e nível de conhecimento individualizado dos alunos. Para complementar o trabalho, é apresentado um protótipo de curso baseado em Máquina de Moore Adaptativa. / This thesis presents a proposal for application of adaptive formalisms for modeling and development of courses for educational software. In principle, adaptive solutions can be incorporated into any type of device guided by rules. In this project, the device will be used behind the Moore Machine, which is a finite automaton with outputs associated with their states. Thus, for each state we can associate the material to be presented by the function output. Applying the concepts of adaptive technology this transducer, you can develop dynamic courses, which are self-modifying based on rules defined by the teacher, and the level of experience and knowledge of individual students. To complement the work is presented a prototype of course based on Adaptive Moore Machine.

Formal verification techniques are growing increasingly vital for the development of safety-critical software and hardware in practice. Techniques such as requirements-based design and model checking for system verification have been successfully used to verify systems for air traffic control, airplane separation assurance, autopilots, CPU logic designs, life-support, medical equipment, and other functions that ensure human safety. Formal behavioral specifications written early in the system-design process and communicated across all design phases increase the efficiency, consistency, and quality of the system under development. We argue that to prevent introducing design or verification errors, it is crucial to test specifications for satisfiability. We advocate for the adaptation of a new sanity check via satisfiability checking for property assurance. Our focus here is on specifications expressed in Linear Temporal Logic (LTL). We demonstrate that LTL satisfiability checking reduces to model checking and satisfiability checking for the specification, its complement, and a conjunction of all properties should be performed as a first step to LTL model checking. We report on an experimental investigation of LTL satisfiability checking. We introduce a large set of rigorous benchmarks to enable objective evaluation of LTL-to-automaton algorithms in terms of scalability, performance, correctness, and size of the automata produced. For explicit model checking, we use the Spin model checker; we tested all LTL-to-explicit automaton translation tools that were publicly available when we conducted our study. For symbolic model checking, we use CadenceSMV, NuSMV, and SAL-SMC for both LTL-to-symbolic automaton translation and to perform the satisfiability check. Our experiments result in two major findings. First, scalability, correctness, and other debilitating performance issues afflict most LTL translation tools. Second, for LTL satisfiability checking, the symbolic approach is clearly superior to the explicit approach. Ironically, the explicit approach to LTL-to-automata had been heavily studied while only one algorithm existed for LTL-to-symbolic automata. Since 1994, there had been essentially no new progress in encoding symbolic automata for BDD-based analysis. Therefore, we introduce a set of 30 symbolic automata encodings. The set consists of novel combinations of existing constructs, such as different LTL formula normal forms, with a novel transition-labeled symbolic automaton form, a new way to encode transitions, and new BDD variable orders based on algorithms for tree decomposition of graphs. An extensive set of experiments demonstrates that these encodings translate to significant, sometimes exponential, improvement over the current standard encoding for symbolic LTL satisfiability checking. Building upon these ideas, we return to the explicit automata domain and focus on the most common type of specifications used in industrial practice: safety properties. We show that we can exploit the inherent determinism of safety properties to create a set of 26 explicit automata encodings comprised of novel aspects including: state numbers versus state labels versus a state look-up table, finite versus infinite acceptance conditions, forward-looking versus backward-looking transition encodings, assignment-based versus BDD-based alphabet representation, state and transition minimization, edge abbreviation, trap-state elimination, and determinization either on-the-fly or up-front using the subset construction. We conduct an extensive experimental evaluation and identify an encoding that offers the best performance in explicit LTL model checking time and is constantly faster than the previous best explicit automaton encoding algorithm.

In this work, hybrid systems with regional dynamics are considered. These are systems where transitions between different dynamical regimes occur as the continuous state of the system reaches given switching surfaces. In particular, the attention is focused on the optimal control problem associated with such systems. More precisely, given a specific cost function, the goal is to determine the optimal path of going from a given starting point to a fixed final state during an a priori specified time horizon. The key characteristic of the approach presented in this thesis is a hierarchical decomposition of the hybrid optimal control problem, yielding to a framework which allows a solution on different levels of control. On the highest level of abstraction, the regional structure of the state space is taken into account and a discrete representation of the connections between the different regions provides global accessibility relations between regions. These are used on a lower level of control to formulate the main theorem of this work, namely, the Hybrid Bellman Equation for multimodal systems, which, in fact, provides a characterization of global optimality, given an upper bound on the number of transitions along a hybrid trajectory. Not surprisingly, the optimal solution is hybrid in nature, in that it depends on not only the continuous control signals, but also on discrete decisions as to what domains the system's continuous state should go through in the first place. The main benefit with the proposed approach lies in the fact that a hierarchical Dynamic Programming algorithm can be used to representing both a theoretical characterization of the hybrid solution's structural composition and, from a more application-driven point of view, a numerically implementable calculation rule yielding to globally optimal solutions in a regional dynamics framework. The operation of the recursive algorithm is highlighted by the consideration of numerous examples, among them, a heterogeneous multi-agent problem.

Το κάτωθι κείμενο πραγματεύεται το φαινόμενο της εξάπλωσης αυτοαναπαραγόμενων αυτομάτων σε δίκτυα. Αρχικά προβαίνουμε σε μια εισαγωγή στα αυτοαναπαραγόμενα προγράμματα και στο περιβάλλον στο οποίο εξαπλώνονται και εν συνεχεία εμβαθύνουμε στον τρόπο με τον οποίο προσεγγίζουμε το φαινόμενο. Μελετάμε μεθόδους ανίχνευσης με χρήση φίλτρων Kalman και εντροπίας. Τέλος, ασχολούμαστε με μια σειρά παιγνίων και σεναρίων με σκοπό την ανάδειξη συγκεκριμένων πλευρών του όλου προβλήματος και την τροπή που παίρνει στις μέρες μας. Εν κατακλείδι, η παρούσα διπλωματική εργασία τονίζει βασικές ιδιότητες που χαρακτηρίζουν την διάδοση και εισάγει νέες βοηθητικές έννοιες και μοντέλα, με στόχο την κατανόηση και τον ενστερνισμό του πνεύματος των εξελίξεων στα σύγχρονα worms και viruses. / The text below considers the phenomenon of propagation of self replicating automata. We begin with an introduction to self replicating programs and to the environment in which they propagate and then we delve and explain the ways of approaching the phenomenon. We study detection methods via the use of Kalman filters and estimation of entropy. Finally, a series of games and scenarios are introduced and studied, in order to enlighten certain aspects of the problem and its current direction. In conclusion, this diploma thesis marks basic properties of the propagation and introduces auxiliary concepts and new models, having as a goal the comprehension and the adoption of the spirit of evolution of modern worms and viruses.