O objetivo deste trabalho é tornar possível a inserção de um robô humanoide para auxiliar pacientes em sessões de fisioterapia. Um sistema robótico é proposto que utiliza um robô humanoide, denominado NAO, visando analisar os movimentos feitos pelos pacientes e corrigi-los se necessário, além de motivá-los durante uma sessão de fisioterapia. O sistema desenvolvido permite que o robô, em primeiro lugar, aprenda um exercício correto de fisioterapia observando sua execução por um fisioterapeuta; em segundo lugar, que ele demonstre o exercício para que um paciente possa imitá-lo; e, finalmente, corrija erros cometidos pelo paciente durante a execução do exercício. O exercício correto é capturado por um sensor Kinect e dividido em uma sequência de estados em dimensão espaço-temporal usando k-means clustering. Estes estados então formam uma máquina de estados finitos para verificar se os movimentos do paciente estão corretos. A transição de um estado para o próximo corresponde a movimentos parciais que compõem o movimento aprendido, e acontece somente quando o robô observa o mesmo movimento parcial executado corretamente pelo paciente; caso contrário o robô sugere uma correção e pede que o paciente tente novamente. O sistema foi testado com vários pacientes em tratamento fisioterapêutico para problemas motores. Os resultados obtidos, em termos de precisão e recuperação para cada movimento, mostraram-se muito promissores. Além disso, o estado emocional dos pacientes foi também avaliado por meio de um questionário aplicado antes e depois do tratamento e durante o tratamento com um software de reconhecimento facial de emoções e os resultados indicam um impacto emocional bastante positivo e que pode vir a auxiliar pacientes durante tratamento fisioterapêuticos. / This dissertation develops a robotic system to guide patients through physiotherapy sessions. The proposed system uses the humanoid robot NAO, and it analyses patients movements to guide, correct, and motivate them during a session. Firstly, the system learns a correct physiotherapy exercise by observing a physiotherapist perform it; secondly, it demonstrates the exercise so that the patient can reproduce it; and finally, it corrects any mistakes that the patient might make during the exercise. The correct exercise is captured via Kinect sensor and divided into a sequence of states in spatial-temporal dimension using k-means clustering. Those states compose a finite state machine that is used to verify whether the patients movements are correct. The transition from one state to the next corresponds to partial movements that compose the learned exercise. If the patient executes the partial movement incorrectly, the system suggests a correction and returns to the same state, asking that the patient try again. The system was tested with multiple patients undergoing physiotherapeutic treatment for motor impairments. Based on the results obtained, the system achieved high precision and recall across all partial movements. The emotional impact of treatment on patients was also measured, via before and after questionnaires and via a software that recognizes emotions from video taken during treatment, showing a positive impact that could help motivate physiotherapy patients, improving their motivation and recovery.

A ideia de usar redes neurais biologicamente inspiradas na computação tem sido amplamente utilizada nas últimas décadas. O fato essencial neste paradigma é que um neurônio pode integrar e processar informações, e esta informação pode ser revelada por sua atividade de pulsos. Ao descrever a dinâmica de um único neurônio usando um modelo matemático, uma rede pode ser implementada utilizando um conjunto desses neurônios, onde a atividade pulsante de cada neurônio irá conter contribuições, ou informações, da atividade pulsante da rede em que está inserido. Neste trabalho é apresentado um controlador de posição no eixo Z utilizando fusão de sensores baseado no paradigma de Redes Neurais Recorrentes. O sistema proposto utiliza uma Máquina de Estado Líquido (LSM) para controlar o robô colaborativo BAXTER. O framework foi projetado para trabalhar em paralelo com as LSMs que executam trajetórias em formas fechadas de duas dimensões, com o objetivo de manter uma caneta de feltro em contato com a superfície de desenho, dados de sensores de força e distância são alimentados ao controlador. O sistema foi treinado utilizando dados de um controlador Proporcional Integral Derivativo (PID), fundindo dados de ambos sensores. Resultados mostram que a LSM foi capaz de aprender o comportamento do controlador PID em diferentes situações. / The idea of employing biologically inspired neural networks to perform computation has been widely used over the last decades. The essential fact in this paradigm is that a neuron can integrate and process information, and this information can be revealed by its spiking activity. By describing the dynamics of a single neuron using a mathematical model, a network in which the spiking activity of every single neuron will get contributions, or information, from the spiking activity of the embedded network. A positioning controller based on Spiking Neural Networks for sensor fusion suitable to run on a neuromorphic computer is presented in this work. The proposed framework uses the paradigm of reservoir computing to control the collaborative robot BAXTER. The system was designed to work in parallel with Liquid State Machines that performs trajectories in 2D closed shapes. In order to keep a felt pen touching a drawing surface, data from sensors of force and distance are fed to the controller. The system was trained using data from a Proportional Integral Derivative controller, merging the data from both sensors. The results show that the LSM can learn the behavior of a PID controller on di erent situations.

A ideia de usar redes neurais biologicamente inspiradas na computação tem sido amplamente utilizada nas últimas décadas. O fato essencial neste paradigma é que um neurônio pode integrar e processar informações, e esta informação pode ser revelada por sua atividade de pulsos. Ao descrever a dinâmica de um único neurônio usando um modelo matemático, uma rede pode ser implementada utilizando um conjunto desses neurônios, onde a atividade pulsante de cada neurônio irá conter contribuições, ou informações, da atividade pulsante da rede em que está inserido. Neste trabalho é apresentado um controlador de posição no eixo Z utilizando fusão de sensores baseado no paradigma de Redes Neurais Recorrentes. O sistema proposto utiliza uma Máquina de Estado Líquido (LSM) para controlar o robô colaborativo BAXTER. O framework foi projetado para trabalhar em paralelo com as LSMs que executam trajetórias em formas fechadas de duas dimensões, com o objetivo de manter uma caneta de feltro em contato com a superfície de desenho, dados de sensores de força e distância são alimentados ao controlador. O sistema foi treinado utilizando dados de um controlador Proporcional Integral Derivativo (PID), fundindo dados de ambos sensores. Resultados mostram que a LSM foi capaz de aprender o comportamento do controlador PID em diferentes situações. / The idea of employing biologically inspired neural networks to perform computation has been widely used over the last decades. The essential fact in this paradigm is that a neuron can integrate and process information, and this information can be revealed by its spiking activity. By describing the dynamics of a single neuron using a mathematical model, a network in which the spiking activity of every single neuron will get contributions, or information, from the spiking activity of the embedded network. A positioning controller based on Spiking Neural Networks for sensor fusion suitable to run on a neuromorphic computer is presented in this work. The proposed framework uses the paradigm of reservoir computing to control the collaborative robot BAXTER. The system was designed to work in parallel with Liquid State Machines that performs trajectories in 2D closed shapes. In order to keep a felt pen touching a drawing surface, data from sensors of force and distance are fed to the controller. The system was trained using data from a Proportional Integral Derivative controller, merging the data from both sensors. The results show that the LSM can learn the behavior of a PID controller on di erent situations.

A realização de atividades de teste é indispensável para a garantia da qualidade de um produto e para a identificação de defeitos, diminuindo custos de manutenção e evitando ao máximo o risco do cliente encontrar esses defeitos. Nessa linha, testes baseados em modelos têm se mostrado atrativos, pois o custo de geração de casos de testes e de correção de defeitos tende a ser menor. Devido à sua simplicidade conceitual e expressividade na descrição do comportamento de um sistema, um dos modelos mais usados e pesquisados na área de teste baseado em modelos são as Máquinas de Estados Finitos (MEFs). Por meio de MEFs e com apoio de ferramentas apropriadas, a geração de casos de testes para avaliar os comportamentos esperados de um sistema é automatizada, reduzindo tanto o custo da geração e da manutenção quanto as falhas humanas. Desta forma, a aplicabilidade de métodos de geração de casos de teste baseados em modelos no contexto de sistemas embarcados vem sendo investigada. O objetivo deste trabalho de mestrado consiste em investigar a aplicabilidade dos métodos de geração em cenários de teste reais, com foco em sistemas embarcados, identificando as difi- culdades e limitações do processo, bem como os requisitos essenciais para a adequação dos métodos de geração propostos na literatura e de ferramentas de apoio à atividade de teste. O foco principal do projeto é a implementação de mecanismos que atendam aos requisitos levantados, visando a usabilidade, segurança e portabilidade da ferramenta / Test activities are essential to ensure the quality of products and identify faults to reduce maintenance costs and avoid that the client finds these faults. In this sense, model-based tests have been proved useful, because the cost of generating test cases and fault correction tend to be smaller. Due to its conceptual simplicity and expressiveness in describing the behavior of a system, Finite State Machines (FSM) have been used and researched in the model-based testing area. FSMs, employed with the support of appropriate tools, enable the generation of test cases in an automated way to assess the expected behavior of a system, reducing both the generation and maintenance costs and human failures. Thus, the applicability of test cases generation methods based on models in the context of embedded systems should be investigated. Test cases generation methods based on FSM are designed to derive test cases from the model. In this context, this work aims to investigate the applicability of generation methods in real-world scenarios, focusing embedded systems. It should identify the difficulties and limitations of the process, as well as the essential requirements for the adequacy of generation methods proposed in the literature and tools to support the test activity. The main focus of the project is the implementation of mechanisms that meet the elicited requirements in order to provide usability, security and tool portability

Os sistemas produtivos (SPs) podem utilizar controladores programáveis (CPs) como dispositivos de realização do controle. Neste contexto, programas de controle executados por estes CPs podem ser desenvolvidos de forma que não estejam em conformidade com as especificações de projeto, o que poderá provocar o surgimento de erros funcionais associados à execução de tais programas de controle, erros estes que podem levar os SPs sob controle a um estado que poderá implicar em acidentes envolvendo equipamentos, pessoas e o meio-ambiente. Esta questão tem motivado o surgimento de diversas abordagens para identificar a existência de erros em programas de controle de CPs, de forma a permitir a correção destes erros e garantir, conseqüentemente, maior confiabilidade operacional. O presente trabalho tem por objetivo identificar a existência de erros em programas de controle baseados em LD (Ladder Diagram). Para isto, propõe-se um procedimento de desenvolvimento de modelos baseados em máquinas de estados finitos estendidas (MEFEs), que são gerados a partir do mapeamento de cada um dos rungs contidos no programa de controle que se deseja identificar erros. Uma vez desenvolvidos os modelos em MEFEs, torna-se possível a utilização de uma ferramenta computacional de verificação, própria para estabelecer se os modelos verificados satisfazem determinadas proposições estabelecidas em lógica temporal. Uma proposição em lógica temporal está relacionada a um estado específico do programa de controle modelado, sendo que o objetivo da verificação é o de estabelecer se a proposição estipulada é atendida ou não. Se um determinado estado específico for, por exemplo, um estado indesejado do programa de controle modelado, e este estado for possível de ser alcançado como resultado do processo de verificação realizado, isto impactará na não conformidade do programa de controle com as especificações comportamentais estipuladas na forma de proposição em lógica temporal, indicando haver, portanto, um erro neste programa de controle modelado. Palavras-chave: Controladores programáveis. Linguagem de programação LD. Modelagem e verificação de máquinas de estados finitos estendidas (MEFEs). / Productive systems (PS) can use programmable logic controllers (PLCs) as the devices of accomplishment of the control. In this context, control programs executed by these PLCs can be developed in a way so that they can be in non-conformity with the project specifications, and this fact may result in functional errors related to the control programs execution. These errors can take the PS under control to a state which can lead into accidents involving equipment, people and the environment. This fact has motivated the appearance of different approaches so as to identify the existence of these errors in PLC control programs so that they can be corrected and assure a greater operational reliability. This work aims at identifying the existence of errors in control programs based on Ladder Diagram (LD). In order to accomplish that, a modeling procedure that generates extended finite state machines (EFSMs) is proposed from the mapping of each one of the rungs in the control program whose errors are to be identified. Once the models based on EFSMs are developed it becomes possible to use a computational verification tool, specifically designed to determine if the verified models fulfill determined propositions established in temporal logic. A proposition in temporal logic is related to a specific state of the modeled control program and the objective of the verification is to establish whether the proposition is fulfilled or not. If a determined specific state, for example, is an unwanted state of the modeled control program and if this state is reachable as a result of the verification process, this will impact in the non-conformity of the control program with the behavior specifications established in a temporal logic proposition, indicating an error in this modeled control program.

Orientador: Arnaldo Vieira Moura / Dissertação (mestrado) - Universidade Estadual de Campinas, Instituto de Computação / Made available in DSpace on 2018-08-16T21:26:35Z (GMT). No. of bitstreams: 1 Pedrosa_LehiltonLelisChaves_M.pdf: 884292 bytes, checksum: e39efddad6809b28790b661469a5cfd2 (MD5) Previous issue date: 2010 / Resumo: Métodos formais são amplamente utilizados para modelar especificações e gerar casos de testes, imprescindíveis para validação de sistemas críticos. As Máquinas de Estados Finitos (MEFs) compõem um dos formalismos adotados, com várias aplicações em testes de sistemas aéreos e espaciais, além de sistemas médicos, entre vários outros. O objetivo de um método de geração automática de casos de testes é obter um conjunto de casos de testes, com o qual é possível verificar se uma dada implementação contém falhas. Um problema importante em métodos de geração de casos de teste com cobertura completa de falhas é o tamanho dos conjuntos de testes, que normalmente é exponencial no número de estados da MEF que está sendo testada. Para minimizar esse problema, diversas abordagens são adotadas, envolvendo melhorias nos métodos existentes, restrições do modelo de falhas e o uso de novas estratégias de teste. Esta dissertação estuda métodos automáticos para geração de casos de testes com cobertura completa de falhas e propõe dois novos métodos, que permitem reduzir o tamanho dos conjuntos de testes gerados. Primeiro, combinamos ideias do método Wp e do método G, visando usufruir as vantagens de ambos e obtendo um novo método, denominado Gp. Em seguida, descrevemos um novo modelo de falhas para sistemas compostos de vários subsistemas, possivelmente com um número alto de estados. Formalizamos tais sistemas, introduzindo o conceito de MEFs combinadas, e apresentamos um novo método de testes, denominado método C. Além disso, propomos uma abordagem de testes incremental, baseada no método C, que torna possível o teste de MEFs com um número arbitrário de estados. Estabelecemos comparações com abordagens tradicionais e mostramos que o uso da estratégia incremental pode gerar conjuntos de testes exponencialmente mais eficientes / Mestrado / Teoria da Computação / Mestre em Ciência da Computação

The field of artificial intelligence has gained much knowledge through the implementation of decision-making systems in video games. One of these systems was the Goal Oriented Action Planning system (GOAP) which directs the behavior of an AI-agent through multiple digital artifacts categorized as goals, actions, and plans. The aim of the thesis is to aid in the understanding and creation of GOAP driven AI-agents in a video game setting to promote research on this topic. The research question of this thesis was about finding out how the GOAP architecture compares to other video game decision-making systems. The theoretical framework introduces the concept of the illusion of intelligence in video games and presents a discussion focused on the different components which make up a GOAP system and other components that support it. Additionally, the theoretical framework explains the need for a comparison between different decision-making systems and explains the social impact of game AI research. The methods section introduces the criteria for the comparison between GOAP and other decision-making systems and presents a comparison process that was driven by a literature review. A GOAP system was designed for this thesis using the unified modeling language and concept maps. It was then implemented using C# code in a free-of-charge game engine called Unity. We present the pseudocode for the implementation of the GOAP system and show that this framework is a modular, customizable, and reusable system that enables AI-agents to create plans from a varied set of actions. Finally, the paper suggests further research within game decision-making AI and emphasizes the importance of game AI research for communities of game developers, hobbyists, and others who could benefit from game AI in their projects.

Unmanned aircraft systems (UASs) are an important future technology with early generations already being used in many areas of application encompassing both military and civilian domains. This thesis proposes a number of integration techniques for combining control-based navigation with more abstract path planning functionality for UASs. These techniques are empirically tested and validated using an RMAX helicopter platform used in the UASTechLab at Linköping University. Although the thesis focuses on helicopter platforms, the techniques are generic in nature and can be used in other robotic systems. At the control level a navigation task is executed by a set of control modes. A framework based on the abstraction of hierarchical concurrent state machines for the design and development of hybrid control systems is presented. The framework is used to specify  reactive behaviors and for sequentialisation of control modes. Selected examples of control systems deployed on UASs are presented. Collision-free paths executed at the control level are generated by path planning algorithms.We propose a path replanning framework extending the existing path planners to allow dynamic repair of flight paths when new obstacles or no-fly zones obstructing the current flight path are detected. Additionally, a novel approach to selecting the best path repair strategy based on machine learning technique is presented. A prerequisite for a safe navigation in a real-world environment is an accurate geometrical model. As a step towards building accurate 3D models onboard UASs initial work on the integration of a laser range finder with a helicopter platform is also presented. Combination of the techniques presented provides another step towards building comprehensive and robust navigation systems for future UASs.

In the area of Discrete Event Systems (DES), formal verification techniques are important in examining a variety of system properties including controllability and nonblocking. Nonetheless, in reality, most software and hardware practitioners are not proficient in formal methods which holds them back from the formal representation and verification of their systems. Alternatively, it is a common observation that control engineers are typically familiar with Moore synchronous Finite State Machines (FSM) and use them to express their controllers’ behaviour. Taking this into consideration, we devise a generic and structured approach to automatically translate Moore synchronous FSM into timed DES (TDES) supervisors. In this thesis, we describe our FSM-TDES translation method, present a set of algorithms to realize the translation steps and rules, and demonstrate the application and correctness of our translation approach with the help of an example. In order to develop our automatic FSM-TDES translation approach, we exploit the structural similarity created by the sampled-data (SD) supervisory control theory between the two models. To build upon the SD framework, first we address a related issue of disabling the tick event in order to force an eligible prohibitable event in the SD framework. To do this, we introduce a new synchronization operator called the SD synchronous product (||SD), adapt the existing TDES and SD properties, and devise our ||SD setting. We formally verify the controllability and nonblocking properties of our ||SD setting by establishing logical equivalence between the existing SD setting and our ||SD setting. We present algorithms to implement our ||SD setting in the DES research tool, DESpot. The formulation of the ||SD operator provides twofold benefits. First, it simplifies the design logic of the TDES supervisors that are modelled in the SD framework. This results in improving the ease of manually designing SD controllable TDES supervisors, and reduced verification time of the closed-loop system. We demonstrate these benefits by applying our ||SD setting to an example system. Second, it bridges the gap between theoretical supervisors and physical controllers with respect to event forcing. This makes our FSM-TDES translation approach relatively uncomplicated. Our automatic FSM-TDES translation approach enables the designers to obtain a formal representation of their controllers without designing TDES supervisors by hand and without requiring formal methods expertise. Overall, this work should increase the adoption of the SD supervisory control theory in particular, and formal methods in general, in the industry by facilitating software and hardware practitioners in the formal representation and verification of their control systems. / Dissertation / Doctor of Philosophy (PhD)

Les codes source-canal conjoints sont des codes réalisant simultanément une compression de données et une protection du train binaire généré par rapport à d’éventuelles erreurs de transmission. Ces codes sont non-linéaires, comme la plupart des codes de source. Leur intérêt potentiel est d’offrir de bonnes performances en termes de compression et de correction d’erreur pour des longueurs de codes réduites.La performance d’un code de source se mesure par la différence entre l’entropie de la source à compresser et le nombre moyen de bits nécessaire pour coder un symbole de cette source. La performance d’un code de canal se mesure par la distance minimale entre mots de codes ou entre suite de mots de codes, et plus généralement à l’aide du spectre des distances. Les codes classiques disposent d’outils pour évaluer efficacement ces critères de performance. Par ailleurs, la synthèse de bons codes de source ou de bons codes de canal est un domaine largement exploré depuis les travaux de Shannon. Par contre des outils analogues pour des codes source-canal conjoints, tant pour l’évaluation de performance que pour la synthèse de bons codes restaient à développer, même si certaines propositions ont déjà été faites dans le passé.Cette thèse s’intéresse à la famille des codes source-canal conjoints pouvant être décrits par des automates possédant un nombre fini d’états. Les codes quasi-arithmétiques correcteurs d’erreurs et les codes à longueurs variables correcteurs d’erreurs font partie de cette famille. La manière dont un automate peut être obtenu pour un code donné est rappelée.A partir d’un automate, il est possible de construire un graphe produit permettant de décrire toutes les paires de chemins divergeant d'un même état et convergeant vers un autre état. Nous avons montré que grâce à l’algorithme de Dijkstra, il est alors possible d’évaluer la distance libre d’un code conjoint avec une complexité polynomiale.Pour les codes à longueurs variables correcteurs d’erreurs, nous avons proposé des bornes supplémentaires, faciles à évaluer. Ces bornes constituent des extensions des bornes de Plotkin et de Heller aux codes à longueurs variables. Des bornes peuvent également être déduites du graphe produit associé à un code dont seule une partie des mots de codes a été spécifiée.Ces outils pour borner ou évaluer exactement la distance libre d’un code conjoint permettent de réaliser la synthèse de codes ayant des bonnes propriétés de distance pour une redondance donnée ou minimisant la redondance pour une distance libre donnée.Notre approche consiste à organiser la recherche de bons codes source-canal conjoints à l’aide d’arbres. La racine de l’arbre correspond à un code dont aucun bit n’est spécifié, les feuilles à des codes dont tous les bits sont spécifiés, et les nœuds intermédiaires à des codes partiellement spécifiés. Lors d’un déplacement de la racine vers les feuilles de l’arbre, les bornes supérieures sur la distance libre décroissent, tandis que les bornes inférieures croissent. Ceci permet d’appliquer un algorithme de type branch-and-prune pour trouver le code avec la plus grande distance libre, sans avoir à explorer tout l’arbre contenant les codes. L'approche proposée a permis la construction de codes conjoints pour les lettres de l'alphabet. Comparé à un schéma tandem équivalent (code de source suivi d'un code convolutif), les codes obtenus ont des performances comparables (taux de codage, distance libre) tout en étant moins complexes en termes de nombre d’état du décodeur.Plusieurs extensions de ces travaux sont en cours : 1) synthèse de codes à longueurs variables correcteurs d’erreurs formalisé comme un problème de programmation linéaire mixte sur les entiers ; 2) exploration à l’aide d’un algorithme de type A* de l’espace des codes de à longueurs variables correcteur d’erreurs. / Joint source-channel codes are codes simultaneously providing data compression and protection of the generated bitstream from transmission errors. These codes are non-linear, as most source codes. Their potential is to offer good performance in terms of compression and error-correction for reduced code lengths.The performance of a source code is measured by the difference between the entropy of the source to be compressed and the average number of bits needed to encode a symbol of this source. The performance of a channel code is measured by the minimum distance between codewords or sequences of codewords, and more generally with the distance spectrum. The classic codes have tools to effectively evaluate these performance criteria. Furthermore, the design of good source codes or good channel codes is a largely explored since the work of Shannon. But, similar tools for joint source-channel codes, for performances evaluation or for design good codes remained to develop, although some proposals have been made in the past.This thesis focuses on the family of joint source-channel codes that can be described by automata with a finite number of states. Error-correcting quasi-arithmetic codes and error-correcting variable-length codes are part of this family. The way to construct an automaton for a given code is recalled.From an automaton, it is possible to construct a product graph for describing all pairs of paths diverging from some state and converging to the same or another state. We have shown that, using Dijkstra's algorithm, it is possible to evaluate the free distance of a joint code with polynomial complexity. For errors-correcting variable-length codes, we proposed additional bounds that are easy to evaluate. These bounds are extensions of Plotkin and Heller bounds to variable-length codes. Bounds can also be deduced from the product graph associated to a code, in which only a part of code words is specified.These tools to accurately assess or bound the free distance of a joint code allow the design of codes with good distance properties for a given redundancy or minimizing redundancy for a given free distance. Our approach is to organize the search for good joint source-channel codes with trees. The root of the tree corresponds to a code in which no bit is specified, the leaves of codes in which all bits are specified, and the intermediate nodes to partially specified codes. When moving from the root to the leaves of the tree, the upper bound on the free distance decreases, while the lower bound grows. This allows application of an algorithm such as branch-and-prune for finding the code with the largest free distance, without having to explore the whole tree containing the codes.The proposed approach has allowed the construction of joint codes for the letters of the alphabet. Compared to an equivalent tandem scheme (source code followed by a convolutional code), the codes obtained have comparable performance (rate coding, free distance) while being less complex in terms of the number of states of the decoder. Several extensions of this work are in progress: 1) synthesis of error-correcting variable-length codes formalized as a mixed linear programming problem on integers, 2) Explore the search space of error-correcting variable-length codes using an algorithm such as A* algorithm.