Orientador: Fabricio Aparecido Breve / Banca: Eraldo Pereira Marinho / Banca: Fernando Vernal Salina / Resumo: A segmentação de imagens é o processo de identificar e separar estruturas e objetos relevantes em uma imagem, não é uma tarefa trivial para um algoritmo computacional devido à complexidade dos elementos envolvidos no processo. A variedade de imagens e sua grande quantidade de características impossibilitam a utilização de apenas um modelo para a tarefa de segmentação. Deste modo, a aplicação de algoritmos de aprendizado de máquina, ganha importância, pois este ramo da inteligência artificial tenta reproduzir a forma de "aprender" humano. A aplicação do modelo de competição e cooperação entre partículas na segmentação de imagens mostra-se uma abordagem interessante pois possui baixo custo computacional, além de reduzir a necessidade de especialistas para a geração de dados rotulados. Este trabalho propõe melhorias na construção da rede complexa que o modelo de competição e cooperação entre partículas utiliza-se, através da alteração das características extraídas dos píxeis, mudança na forma de ligação dos vértices do modelo utilizando a similaridade das características e a vizinhança espacial dos píxeis da imagem e a influência gerada por uma partícula sob outros vértices vizinhos dentro da rede complexa. A metodologia proposta resultou em uma melhoria do nível de automação do processo, eliminando a necessidade de incrementar ou decrementar a importância de uma característica sob as outras. Comparativamente, durante os testes realizados com 151 imagens e 4530 amostras de... / Abstract: Image segmentation is the process of identifying and separating relevant structures and objects in an image, it is not a trivial task for a computational algorithm due to the complexity of the elements involved in the process. The variety of images and its vast number of characteristics make it impossible to use only a model for the segmentation task. In this way, the application of machine learning algorithms is highlighted, because this branch of artificial intelligence tries to reproduce the way of human learning. The application of the competition and cooperation model among particles in the image segmentations is considered an interesting approach since it has low computational cost, besides reducing the need of specialists for generating labeled data. This work proposes improvements in the making of the complex network that the competition and cooperation model among particles uses, through the alteration of the characteristics extracted from pixels, changes in the shape of the model's connection of the vertices using the similarity of the characteristics and the image pixel's spatial neighboring and the influence generated by a particle under the other neighbor vertices within the complex network. The proposed methodology resulted in an improvement of the process's automation level, eliminating the need to increase or decrease the importance of a characteristic under others. Comparatively, during the tests made with 151 images and 4530 execution samples for each ... / Mestre

Orientador: Alexandro José Baldassin / Banca: Adriane Beatriz de Souza Serapião / Banca: Fátima de Lourdes dos Santos Nunes / Resumo: O presente trabalho visa a construção de uma ferramenta de auxílio para profissionais da fisioterapia, que promova por meio de tecnologias da computação, como a lógica Fuzzy, um tratamento personalizado, motivador e eficaz. Inicialmente fez-se uma verificação da literatura e trabalhos que relacionem reabilitação com tecnologia (incluindo ambientes virtuais imersivos e não imersivos), seguida de uma análise das necessidades da fisioterapia para, enfim, criar uma proposta de solução computacional. O problema encontrado consiste da necessidade de uma ferramenta motivadora (mantenha a assiduidade do paciente), que apresente dados da progressão do paciente e seja de fácil utilização (pelo paciente e fisioterapeuta). A solução computacional envolve câmera de profundidade e sensores vestíveis para obter dados corporais e, com análise de dados e utilização de métodos de inteligência artificial, consiga prover uma forma intuitiva, motivadora e eficiente para o tratamento fisioterapêutico. Resultados mostram a aplicabilidade da proposta em obter os valores biométricos, a criação de exercícios personalizados, os jogos motivacionais com dificuldade dinâmica por meio da lógica Fuzzy proposta e a visualização do progresso dos pacientes / Abstract: The present work aims to build an assist tool to physiotherapists that, through computer science technologies, such as Fuzzy logic, can promote a personalized, motivating and efficient treatment. Initially a literature review and works related to technologies and health were analyzed, followed by an analysis of the physiotherapy needs so that a computer solution could be proposed. The issue found consists in the need of a motivational tool (which can keep the attendance of the patient), that shows progressive data of the patient and is of ease use (both by the patient and physiotherapist). The computer solution uses a depth camera (such as MS Kinect) and wearable sensors to obtain the body data and, through data analysis and artificial intelligence methods, make an intuitive, motivational and efficient solution for the physical treatment. Results shows the applicability of the proposal in obtaining the biometric data, the creation of custom virtual exercises, the motivational games with dynamic difficulty through the Fuzzy logic and the visualization of the patient progress / Mestre

The aim of this thesis is to present an extension to the string graphs of Dixon, Duncan and Kissinger that allows the finite representation of certain infinite families of graphs and graph rewrite rules, and to demonstrate that a logic can be built on this to allow the formalisation of inductive proofs in the string diagrams of compact closed and traced symmetric monoidal categories. String diagrams provide an intuitive method for reasoning about monoidal categories. However, this does not negate the ability for those using them to make mistakes in proofs. To this end, there is a project (Quantomatic) to build a proof assistant for string diagrams, at least for those based on categories with a notion of trace. The development of string graphs has provided a combinatorial formalisation of string diagrams, laying the foundations for this project. The prevalence of commutative Frobenius algebras (CFAs) in quantum information theory, a major application area of these diagrams, has led to the use of variable-arity nodes as a shorthand for normalised networks of Frobenius algebra morphisms, so-called "spider notation". This notation greatly eases reasoning with CFAs, but string graphs are inadequate to properly encode this reasoning. This dissertation firstly extends string graphs to allow for variable-arity nodes to be represented at all, and then introduces !-box notation – and structures to encode it – to represent string graph equations containing repeated subgraphs, where the number of repetitions is abitrary. This can be used to represent, for example, the "spider law" of CFAs, allowing two spiders to be merged, as well as the much more complex generalised bialgebra law that can arise from two interacting CFAs. This work then demonstrates how we can reason directly about !-graphs, viewed as (typically infinite) families of string graphs. Of particular note is the presentation of a form of graph-based induction, allowing the formal encoding of proofs that previously could only be represented as a mix of string diagrams and explanatory text.

In vitro tissue engineering is a method for developing living and functional tissues external to the body, often within a device called a bioreactor to control the chemical and mechanical environment. However, the quality of bone tissue engineered products is currently inadequate for clinical use as the implant cannot bear weight. In an effort to improve the quality of the construct, hydrostatic pressure, the pressure in a fluid at equilibrium that is required to balance the force exerted by the weight of the fluid above, has been investigated as a mechanical stimulus for promoting extracellular matrix deposition and mineralisation within bone tissue. Thus far, little research has been performed into understanding the response of bone tissue cells to mechanical stimulation. In this thesis we investigate an in vitro bone tissue engineering experimental setup, whereby human mesenchymal stem cells are seeded within a collagen gel and cultured in a hydrostatic pressure bioreactor. In collaboration with experimentalists a suite of mathematical models of increasing complexity is developed and appropriate numerical methods are used to simulate these models. Each of the models investigates different aspects of the experimental setup, from focusing on global quantities of interest through to investigating their detailed local spatial distribution. The aim of this work is to increase understanding of the underlying physical processes which drive the growth and development of the construct, and identify which factors contribute to the highly heterogeneous spatial distribution of the mineralised extracellular matrix seen experimentally. The first model considered is a purely temporal model, where the evolution of cells, solid substrate, which accounts for the initial collagen scaffold and deposited extracellular matrix along with attendant mineralisation, and fluid in response to the applied pressure are examined. We demonstrate that including the history of the mechanical loading of cells is important in determining the quantity of deposited substrate. The second and third models extend this non-spatial model, and examine biochemically and biomechanically-induced spatial patterning separately. The first of these spatial models demonstrates that nutrient diffusion along with nutrient-dependent mass transfer terms qualitatively reproduces the heterogeneous spatial effects seen experimentally. The second multiphase model is used to investigate whether the magnitude of the shear stresses generated by fluid flow, can qualitatively explain the heterogeneous mineralisation seen in the experiments. Numerical simulations reveal that the spatial distribution of the fluid shear stress magnitude is highly heterogeneous, which could be related to the spatial heterogeneity in the mineralisation seen experimentally.

Introduction: Antimalarial resistance, particularly artemisinin resistance, is a major threat to P. falciparum malaria elimination efforts worldwide. Urgent intervention is required to tackle artemisinin resistance but field data on which to base planning of strategies are limited. The aims were to collect available field data and develop population level mathematical models of P. falciparum malaria treatment and artemisinin resistance in order to determine the optimal strategies for elimination of artemisinin resistant malaria in Cambodia and treatment of pre-hospital and severe malaria in Cambodia and Bangladesh. Methods: Malaria incidence and parasite clearance data from Cambodia and Bangladesh were collected and analysed and modelling parameters derived. Population dynamic mathematical models of P. falciparum malaria were produced. Results: The modelling demonstrated that elimination of artemisinin resistant P. falciparum malaria would be achievable in Cambodia in the context of artemisinin resistance using high coverages with ACT treatment, ideally combined with LLITNs and adjunctive single dose primaquine. Sustained efforts would be necessary to achieve elimination and effective surveillance is essential, both to identify the baseline malaria burden and to monitor parasite prevalence as interventions are implemented. A modelled policy change to rectal and intravenous artesunate in the context of pre-existing artemisinin resistance would not compromise the efficacy of ACT for malaria elimination. Conclusions: By being developed rapidly in response to specific questions the models presented here are helping to inform planning efforts to combat artemisinin resistance. As further field data become available, their planned on-going development will produce increasingly realistic and informative models which can be expected to play a central role in planning efforts for years to come.

In this dissertation, we study the verification of concurrent programs written in the programming language Erlang using infinite-state model-checking. Erlang is a widely used, higher order, dynamically typed, call-by-value functional language with algebraic data types and pattern-matching. It is further augmented with support for actor concurrency, i.e. asynchronous message passing and dynamic process creation. With decidable model-checking in mind, we identify actor communicating systems (ACS) as a suitable target model for an abstract interpretation of Erlang. ACS model a dynamic network of finite-state processes that communicate over a fixed, finite number of unordered, unbounded channels. Thanks to being equivalent to Petri nets, ACS enjoy good algorithmic properties. We develop a verification procedure that extracts a sound abstract model, in the form of an ACS, from a given Erlang program; the resulting ACS simulates the operational semantics of the input. Using this abstract model, we can conservatively verify coverability properties of the input program, i.e. a weak form of safety properties, with a Petri net model-checker. We have implemented this procedure in our tool Soter, which is the first sound verification tool for Erlang programs using infinite-state model-checking. In our experiments, we find that Soter is accurate enough to verify a range of interesting and non-trivial benchmarks. Even though ACS coverability is Expspace-complete, Soter's analysis of these verification problems is surprisingly quick. In order to improve the precision of our verification procedure with respect to recursion, we investigate an extension of ACS that allows pushdown processes: asynchronously communicating pushdown systems (ACPS). ACPS that satisfy the empty-stack constraint (a pushdown process may receive only when its stack is empty) are a popular subclass of ACPS with good decision and complexity properties. In the context of Erlang, the empty stack constraint is unfortunately not realistic. We introduce a relaxation of the empty-stack constraint for ACPS called the shaped stack constraint. Stacks that fit the shape constraint may reach arbitrary heights. Further, a process may execute any communication action (be it process creation, message send or retrieval) whether or not its stack is empty. We prove that coverability for shaped ACPS, i.e. ACPS that satisfy the shaped constraint, reduces to the decidable coverability problem for well-structured transition systems (WSTS). Thus, shaped ACPS enable the modelling and verification of a larger class of message passing programs. We establish a close connection between shaped ACPS and a novel extension of Petri nets: nets with nested coloured tokens (NNCT). Tokens in NNCT are of two types: simple and complex. Complex tokens carry an arbitrary number of coloured tokens. The rules of a NNCT can synchronise complex and simple tokens, inject coloured tokens into a complex token, and eject all tokens of a specified set of active colours to predefined places. We show that the coverability problem for NNCT is Tower-complete, a new complexity class for non-elementary decision problems introduced by Schmitz. To prove Tower-membership, we devise a geometrically inspired version of the Rackoff technique, and we obtain Tower-hardness by adapting Stockmeyer's ruler construction to NNCT. To our knowledge, NNCT is the first extension of Petri nets (belonging to the class of nets with an infinite set of token types) that is proven to have primitive recursive coverability. This result implies Tower-completeness of coverability for ACPS that satisfy the shaped stack constraint.

Krivelevich and Patkós conjectured in 2009 that χ(G(n, p)) ∼ χ=(G(n, p)) ∼ χ∗=(G(n, p)) for C/n < p < 1 − ε, where ε > 0. We prove this conjecture for n−1+ε1 < p < 1 − ε2 where ε1, ε2 > 0. We investigate several measures that have been proposed to indicate centrality of nodes in networks, and find examples of networks where they fail to distinguish any of the vertices nodes from one another. We develop a new method to investigate core-periphery structure, which entails identifying densely-connected core nodes and sparsely-connected periphery nodes. Finally, we present an experiment and an analysis of empirical networks, functional human brain networks. We found that reconfiguration patterns of dynamic communities can be used to classify nodes into a stiff core, a flexible periphery, and a bulk. The separation between this stiff core and flexible periphery changes as a person learns a simple motor skill and, importantly, it is a good predictor of how successful the person is at learning the skill. This temporally defined core-periphery organisation corresponds well with the core- periphery detected by the method that we proposed earlier the static networks created by averaging over the subjects dynamic functional brain networks.

In this thesis we describe subclasses of a class of graphs with three types of edges, called loopless mixed graphs (LMGs). The class of LMGs contains almost all known classes of graphs used in the literature of graphical Markov models. We focus in particular on the subclass of ribbonless graphs (RGs), which as special cases include undirected graphs, bidirected graphs, and directed acyclic graphs, as well as ancestral graphs and summary graphs. We define a unifying interpretation of independence structure for LMGs and pairwise and global Markov properties for RGs, discuss their maximality, and, in particular, prove the equivalence of pairwise and global Markov properties for graphoids defined over the nodes of RGs. Three subclasses of LMGs (MC, summary, and ancestral graphs) capture the modified independence model after marginalisation over unobserved variables and conditioning on selection variables of variables satisfying independence restrictions represented by a directed acyclic graph (DAG). We derive algorithms to generate these graphs from a given DAG or from a graph of a specific subclass, and we study the relationships between these classes of graphs. Finally, a manual and codes are provided that explain methods and functions in R for implementing and generating various graphs studied in this thesis.

This thesis presents a finite element methodology for simulating fluid–solid interactions in the left ventricle (LV) under LVAD support. The developed model was utilised to study the passive and active characteristics of ventricular function in anatomically accurate LV geometries constructed from normal and patient image data. A non–conforming ALE Navier–Stokes/finite–elasticity fluid–solid coupling system formed the core of the numerical scheme, onto which several novel numerical additions were made. These included a fictitious domain (FD) Lagrange multiplier method to capture the interactions between immersed rigid bodies and encasing elastic solids (required for the LVAD cannula), as well as modifications to the Newton–Raphson/line search algorithm (which provided a 2 to 10 fold reduction in simulation time). Additional developments involved methods for extending the model to ventricular simulations. This required the creation of coupling methods, for both fluid and solid problems, to enable the integration of a lumped parameter representation of the systemic and pulmonary circulatory networks; the implementation and tuning of models of passive and active myocardial behaviour; as well as the testing of appropriate element types for coupling non–conforming fluid– solid finite element models under high interface tractions (finding that curvilinear spatial interpolations of the fluid geometry perform best). The behaviour of the resulting numerical scheme was investigated in a series of canonical test problems and found to be convergent and stable. The FD convergence studies also found that discontinuous pressure elements were better at capturing pressure gradients across FD boundaries. The ventricular simulations focused firstly on studying the passive diastolic behaviour of the LV both with and without LVAD support. Substantially different vortical flow features were observed when LVAD outflow was included. Additionally, a study of LVAD cannula lengths, using a particle tracking algorithm to determine recirculation rates of blood within the LV, found that shorter cannulas improved the recirculation of blood from the LV apex. Incorporating myocardial contraction, the model was extended to simulate the full cardiac cycle, converging on a repeating pressure–volume loop over 2 heart beats. Studies on the normal LV geometry found that LVAD implementation restricts the recirculation of early diastolic inflow, and that fluid–solid coupled models introduce greater heterogeneity of myocardial work than was observed in equivalent solid only models. A patient study was undertaken using a myocardial geometry constructed using image data from an LVAD implant recipient. A series of different LVAD flow regimes were tested. It was found that the opening of the aortic valve had a homogenising effect on the spatial variation of work, indicating that the synchronisation of LVAD outflow with the cardiac cycle is more important if the valve remains shut. Additionally, increasing LVAD outflow during systole and decreasing it during diastole led to improved mixing of blood in the ventricular cavity – compared with either the inverse, or holding outflow constant. Validation of these findings has the potential to impact the treatment protocols of LVAD patients.

Sudden cardiac death is one of the leading causes of mortality in the western world. One of the main factors is myocardial ischaemia, when there is a mismatch between blood demand and supply to the heart, which may lead to disturbed cardiac excitation patterns, known as arrhythmias. Ischaemia is a dynamic and complex process, which is characterised by many electrophysiological changes that vary through space and time. Ischaemia-induced arrhythmic mechanisms, and the safety and efficacy of certain therapies are still not fully understood. Most experimental studies are carried out in animal, due to the ethical and practical limitations of human experiments. Therefore, extrapolation of mechanisms from animal to human is challenging, but can be facilitated by in silico models. Since the first cardiac cell model was built over 50 years ago, computer simulations have provided a wealth of information and insight that is not possible to obtain through experiments alone. Therefore, mathematical models and computational simulations provide a powerful and complementary tool for the study of multi-scale problems. The aim of this thesis is to investigate pro-arrhythmic electrophysiological consequences of acute myocardial ischaemia, using a multi-scale computational modelling and simulation framework. Firstly, we present a novel method, combining computational simulations and optical mapping experiments, to characterise ischaemia-induced spatial differences modulating arrhythmic risk in rabbit hearts. Secondly, we use computer models to extend our investigation of acute ischaemia to human, by carrying out a thorough analysis of recent human action potential models under varied ischaemic conditions, to test their applicability to simulate ischaemia. Finally, we combine state-of-the-art knowledge and techniques to build a human whole ventricles model, in which we investigate how anti-arrhythmic drugs modulate arrhythmic mechanisms in the presence of ischaemia.