Дисертації з теми "Lógica Temporal"

Orientador: Jose Alexandre Durry Guerzoni
Dissertação (mestrado) - Universidade Estadual de Campinas, Instituto de Filosofia e Ciencias Humanas
Made available in DSpace on 2018-07-19T12:28:05Z (GMT). No. of bitstreams: 1 Magossi_JoseCarlos_M.pdf: 10085958 bytes, checksum: 78f696d242fe4880bc35c9334cf34e9c (MD5) Previous issue date: 1994
Resumo: Não informado
Abstract: Not informed.
Mestrado
Mestre em Lógica e Filosofia da Ciência

Dissertação (mestrado) - Universidade Federal de Santa Catarina, Centro Tecnológico, Programa de Pós-Graduação em Ciência da Computação, Florianópolis, 2017.
Made available in DSpace on 2017-11-21T03:19:53Z (GMT). No. of bitstreams: 1 348589.pdf: 6329634 bytes, checksum: 38bb35f6130676e302e7a2b108031d96 (MD5) Previous issue date: 2017
Nos últimos tempos, o sequenciamento de atividades educacionais ocorre por meio de recursos na forma de Objetos de Aprendizagem (OAs), os quais podem ser selecionados para personalizar atividades conforme características específicas do Aprendiz. Apresenta-se aqui a hipótese de que características dinâmicas do Aprendiz podem ser representadas em função de operadores de Lógica Temporal, e mais especificamente, pode-se estabelecer uma relação deste com o Domínio de Conhecimento em um curso. Portanto, estes aspectos temporais somam-se a outras características na identificação do estado corrente do Aprendiz, servem de amparo para a definição do escopo de curso e auxiliam no planejamento de ações futuras. A partir disto, propõe-se um sistema híbrido entre Sistemas Tutores Inteligentes (STI) e Sistemas Hipermídia Adaptativos Educacionais (SHAE), resultando em um sistema, denominado Smart ITS, constituído de uma arquitetura que contém agentes e artefatos. O Agente Tutor do Smart ITS destaca-se por fazer uso de operadores de Lógica Temporal para representar crenças e garantir tanto a flexibilidade, provida com a adaptatividade de OAs, quanto a estrutura robusta do Domínio de Conhecimento em que efetua tutoria. As crenças e as respectivas semânticas temporais que são utilizadas pelo Agente Tutor servem de modelo para planejamento, visto que as mesmas ditam o sequenciamento ordenado de ações através de proposições que representam estados de mundo e que seguem um modelo conceitual com a finalidade de elaboração de planos.
Abstract : In the last years, the sequencing of educational activities occurs through resources in the form of Learning Objects (Los), which can be selected to personalize activities in conformity with the learner specific characteristics. We present as hypothesis that dynamic features can be represented in accordance with Temporal Logic and, more specifically, we can establish a relation from the learner to the course knowledge domain. Therefore, these temporal aspects are added to other characteristics for the current Learner's state identification, supporting the course's scope definition and aiding for planning future actions. Thus, we propose a hybrid Intelligent Tutoring Systems (ITS) and Adaptive Educational Hypermedia Systems (AEHS), resulting in a system, named Smart ITS, consisting of an architecture that contains agents and artifacts. The Tutor Agent in Smart ITS stands out by utilizing Temporal Logic operators to represent beliefs and by granting both flexibility, provided by the adaptability with LOs, and the robust structure of domain knowledge wherein tutoring takes effect. The temporal beliefs and the respective temporal semantics used by the Tutor Agent serve as model for planning, since those same dictate the ordered sequencing of actions through propositions that represent states of the world and follow a conceptual model with the finality of plans elaboration.

Made available in DSpace on 2014-06-12T15:56:09Z (GMT). No. of bitstreams: 2 arquivo2750_1.pdf: 2282996 bytes, checksum: f61a8b47ec62dc124a6eafe258c2c9a0 (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2010
Fundação de Amparo à Ciência e Tecnologia do Estado de Pernambuco
As pesquisas relacionadas à previsão de séries temporais têm sido uma área de bastante interesse nas últimas décadas. Várias técnicas têm sido pesquisadas para a previsão de séries temporais. Este trabalho propõe métodos híbridos, com a finalidade de tentar representar o complexo fenômeno de previsão de séries temporais do mundo real. A gênese do estudo é baseada no conceito sobre o qual, diferentes partes da série temporal podem ser resultantes de diferentes processos físicos que ocorrem na natureza e necessitam, portanto, de diferentes modelagens. A dissertação divide-se em duas etapas. Na primeira, são propostos mais dois sistemas híbridos (BH + MLP e BMT + MLP) para a seleção das variáveis de entradas para os modelos de previsão. Na segunda, são propostas dois métodos híbridos (SOM + MLP e MLP + Fuzzy) para o processo de previsão de séries temporais. Para realizar o estudo comparativo entre as técnicas, dez séries temporais do mundo real foram utilizadas. No que diz respeito à seleção de variáveis os resultados mostraram que a utilização do sistema híbrido Busca pela Memória Temporal e Redes Neurais (BMT + MLP) foi capaz de encontrar um subconjunto de variáveis representativo para o problema. Dos resultados obtidos pode-se concluir que a seleção de variáveis ocorreu de forma bastante satisfatória com a utilização da Busca Harmônica e Redes Neurais, mas ocorreu com maior rapidez e eficiência quando da utilização do sistema proposto BMT + MLP. Apesar dos erros médios quadráticos obtidos pela rede neural serem, em geral, estatisticamente similares para as duas técnicas, a principal vantagem da BMT + MLP é a capacidade de encontrar o subconjunto de variáveis considerado ótimo de forma bastante rápida. Ao realizar a comparação dos resultados obtidos dos modelos propostos com dois modelos da literatura, os modelos propostos apresentaram um melhor desempenho. Quanto aos modelos de previsão propostos, os resultados obtidos apresentaram menor erro ou no máximo iguais em comparação com a rede MLP e com os modelos Estatísticos, para todas as séries simuladas. Por outro lado, os dois modelos propostos (SOM + MLP e MLP + Fuzzy) apresentaram em média resultados que foram considerados estatisticamente similares

A inteligência computacional é considerada por diferentes autores da atualidade como o destino manifesto da Ciência da Computação. A modelagem de diversos aspectos da cognição, tais como aprendizagem e raciocínio, tem sido a motivação para o desenvolvimento dos paradigmas simbólico e conexionista da inteligência artificial e, mais recentemente, para a integração de ambos com o intuito de unificar as vantagens de cada abordagem em um modelo único. Para o desenvolvimento de sistemas inteligentes, bem como para diversas outras áreas da Ciência da Computação, o tempo é considerado como um componente essencial, e a integração de uma dimensão temporal nestes sistemas é fundamental para conseguir uma representação melhor do comportamento cognitivo. Neste trabalho, propomos o SCTL (Sequential Connectionist Temporal Logic), uma abordagem neuro-simbólica para integrar conhecimento temporal, representado na forma de programas em lógica, em redes neurais recorrentes, de forma que a caracterização semântica de ambas representações sejam equivalentes. Além da estratégia para realizar esta conversão entre representações, e da verificação formal da equivalência semântica, também realizamos uma comparação da estratégia proposta com relação a outros sistemas que realizam representação simbólica e temporal em redes neurais. Por outro lado, também descrevemos, de foma algorítmica, o comportamento desejado para as redes neurais geradas, para realizar tanto inferência quanto aprendizagem sob uma ótica temporal. Este comportamento é analisado em diversos experimentos, buscando comprovar o desempenho de nossa abordagem para a modelagem cognitiva considerando diferentes condições e aplicações.
Computational Intelligence is considered, by di erent authors in present days, the manifest destiny of Computer Science. The modelling of di erent aspects of cognition, such as learning and reasoning, has been a motivation for the integrated development of the symbolic and connectionist paradigms of artificial intelligence. More recently, such integration has led to the construction of models catering for integrated learning and reasoning. The integration of a temporal dimension into such systems is a relevant task as it allows for a richer representation of cognitive behaviour features, since time is considered an essential component in intelligent systems development. This work introduces SCTL (Sequential Connectionist Temporal Logic), a neuralsymbolic approach for integrating temporal knowledge, represented as logic programs, into recurrent neural networks. This integration is done in such a way that the semantic characterization of both representations are equivalent. Besides the strategy to achieve translation from one representation to another, and verification of the semantic equivalence, we also compare the proposed approach to other systems that perform symbolic and temporal representation in neural networks. Moreover, we describe the intended behaviour of the generated neural networks, for both temporal inference and learning through an algorithmic approach. Such behaviour is then evaluated by means several experiments, in order to analyse the performance of the model in cognitive modelling under di erent conditions and applications.

In this thesis, we study planning systems based on logics, for two particular cases: Temporal Defeasible Logic Programming t-DeLP and the Logics of Communication and Change LCC. A planning problem consists in building a course of actions, or plan, whose execution leads from a given initial state to some goal state. The motivation for the present studies, from the point of view of Logic, is to obtain systems for practical reasoning (what an agent should do) from given logics oriented to multi-agent systems. From the Artificial Intelligence point of view, the motivation consists in extending the languages and logics underlying the well-known classical or temporal planning systems. This way, a planner can correctly reason about certain concepts (actions, causality, belief, etc.) using an appropriate logic to this end. In practice, the proposed methods permit a planner to aim for goals which can be expressed in the corresponding logical languages. The first part of the thesis contains a study of t-DeLP along these lines. The t-DeLP framework is a non-monotonic temporal logic programming system based on tools from computational argumentation. This logic system aimsto model different types of causal reasoning in a non-monotonic way, but using to this end natural concepts inspired by human reasoning and argumentation. The t-DeLP system is a temporal extension of the DeLP system proposed by García and Simari. In t-DeLP, a knowledge base is given by a set of temporal rules and facts, which combine into arguments (or consistent, minimal derivations) for further derived temporal facts (or conclusions). The language admits two types of rules: strict and defeasible. The former behave similarly to rules in monotonic logics, while derivations or arguments making use of some defeasible rules can be canceled by other existing arguments. To solve the temporal inconsistencies between conflicting arguments, we propose two criteria based on a preference for arguments using more strict facts (more basic information) or less persistence rules. It is shown that the resulting logic programming system satisfies different consistency and closure properties that any logic-argumentation system should obey. In order to define a planning system based on t-DeLP, one can introduce temporal actions as pairs of preconditions and effects. These actions combine with the t-DeLP consequence relation, thus inducing a state transition system. Different search algorithms for centralized planning can be shown to be sound and complete for the class of planning problems definable in t-DeLP. We also study the decentralized case, where a group of planning agents cooperate in order to reach an agreement upon a joint plan for their shared goals. For this, we propose a protocol for argumenative dialogues that defines a plan search algorithm. This algorithm is also shown to be sound and complete, with respect to centralized planning. The second part of the thesis focuses on the Logics of Communication and Change, or LCC. LCC is a family of dynamic epistemic logics proposed by van Benthem et al. Which capture a good deal of the existing dynamic epistemic logics in the literature. The class of LCC modal logics contain a rich class of epistemic operators for multiple agents or groups as well as operators for common knowledge or belief. They also contain dynamic operators for the execution of epistemic actions (communications, observations) or physical actions. The actions of either type can also be modelled with their epistemic effects, that is, how the action will appear to each of the agents. In this thesis, we also extend these logics with product and choice constructors in order to model non-deterministic actions and plans. We propose a simple extension of the axiom system along this line, and show its soundndess and completeness. The proposed planning system based on these logics permit the study of deterministic and non-deterministic planning. In this thesis we show that the corresponding search algorithms based on Breadth First Search are correct and complete for backward planning in a given LCC logic. This is shown for both the deterministic case, and for strong non-deterministic planning.
En aquesta tesi, estudiem algorismes de planificació per a dues lògiques enfocades a sistemes multi-agent. Amb més detall, estudiem problemes de planificació (com arribar a estats objectiu a partir de l'estat inicial i un conjunt d'accions disponibles), els elements dels quals es poden expressar en alguna de les dues lògiques. En la primera part de la tesi, proposem en primer lloc una extensió temporal de la programació lògica rebatible (temporal defeasible logic programming) t-DeLP. Aquest és un sistema de programació lògica no-monotònica basat en tècniques d'argumentació i orientat al raonament sobre les accions, i especialment dels seus efectes indirectes. En el llenguatge d'aquesta lògica, hom pot descriure accions temporals de l'estil de sistemes de planificació, i definir al seu temps un sistema de transicions d'estats. Finalment, això permet definir un sistema de planificació basat en aquesta lògica que combina accions i derivacions lògiques. Les contribucions principals al respecte són: l'estudi de les propietats argumentatives del sistema lògic, i de la correcció i completesa d'algorismes basats en Breadth First Search de cerca en l'espai de plans. En la segona part de la tesi, estudiem sistemes de planificació definits sobre una família de lògiques dinàmiques epistèmiques, conegudes com a Logics of Communication and Change. Aquestes lògiques permeten l'estudi formal de les creences de diversos agents, així com dels efectes epistemics i físics de diferents tipus d'accions. Entre aquestes, podem incloure diferents accions comunicatives (públiques, privades), observacions i les accions físiques habituals en planning. L'estudi del sistema de planificació definit per aquestes lògiques és dut a terme mitjançant algorismes de cerca basats en breadth first search. Les contribucions principals són l'extensió d'aquestes lògiques amb accions no-deterministes i composició d'accions, i la demostració de la correcció

O conhecimento da probabilidade de ocorrência de precipitações é de grande importância para o planejamento de atividades como produção agrícola, sistemas de abastecimento de água e geração de energia. Neste sentido, a análise regional de freqüências se apresenta como uma ferramenta para a redução de incertezas na estimativa das probabilidades, podendo também diminuir a dimensionalidade das informações. Desta forma, esta pesquisa tem por objetivo estudar uma metodologia para análise regional de freqüências, aplicada à precipitação, na qual se admite que as séries que formam uma região homogênea seguem uma mesma distribuição, que dispensa a utilização de fatores de escala locais, e que seus parâmetros podem ser satisfatoriamente estimados pela média dos parâmetros de ajuste das séries locais. Para compor a metodologia foi construído um teste de homogeneidade regional e um teste para avaliar a qualidade do agrupamento, que leva em consideração os objetivos da análise. Os dois testes citados e a verificação da qualidade da obtenção da distribuição regional pela média dos parâmetros locais foram baseados na medida da máxima diferença de probabilidades entre duas séries e no teste de aderência de Kolmogorov-Smirnov (KS), auxiliando, então, numa melhor compreensão dos resultados, já que esse teste é referência na avaliação da qualidade do ajuste de funções probabilísticas. Como estudo de caso, a metodologia foi aplicada na análise de precipitações totais mensais e anuais no Rio Grande do Sul e em Santa Catarina, utilizando-se o método de agrupamento difuso Fuzzy CMeans para identificação das regiões. Verificou-se que o modelo de obtenção da distribuição regional proposto é satisfatório, embora necessite de um fator de correção para a distribuição Gama. O teste de aderência regional mostrou-se bastante útil para orientar a ponderação das variáveis e para auxiliar na determinação do melhor número de regiões, o que foi comprovado pelo alto grau de homogeneidade verificado, mesmo antes de serem aplicados ajustes nas regiões resultantes do agrupamento. Constatou-se ainda que a utilização dos graus de pertinência não produziu resultados satisfatórios para fazer estimativas pontuais e pouco contribuiu para a realização de ajustes no agrupamento. Todavia, o ajuste do modelo de alocação para novos pontos, através da matriz de pertinência, apresentou bons resultados, embora ainda seja necessária sua verificação em situação real. A análise regional da área de estudo resultou em nove regiões, que foram consideradas heterogêneas em apenas dois dos 117 períodos avaliados. Além disso, a partir do teste KS ( = 20%), verificou-se que as distribuições regionais se mostraram válidas para 97,8% das séries, confirmando a possibilidade de utilizar a distribuição regional, sem a necessidade dos fatores de escala locais.
Information on rainfall probability are helpful for some activities planning including agriculture, water supply and hydropower generation. For such purpose, the regional frequency analysis is a powerful tool to reduce uncertainties in probabilities estimation and also information’s dimension. This research evaluates the possibility of taking rainfall regional frequency analysis considering that in a homogeneous region the site frequency distributions are identical, setting aside local scaling factors, and that its parameters may satisfactorily be estimated by average parameters of local series fitting. To address such goals, the methodology consisted of elaborating a regional homogeneity test and a test to assess the cluster quality. Both tests and the assessment over the regional distribution quality were based on the maximum probability differences between two series and on the Kolmogorov-Smirnov test (KS). As a case study, the methodology was applied on Rio Grande do Sul and Santa Catarina States monthly and annual precipitation data, using clustering method Fuzzy CMeans for identification of regions. It was verified that the regional distribution model is satisfactory, although it needs a correction factor for Gamma distribution. The test of regional adherence was useful to guide the variables weighting and to help on the determination of the optimum number of regions, once a high degree of homogeneity was obtained, even before the application of adjustments on the resultant regions from the cluster analysis. The use of membership degrees was not satisfactory on estimating at-site features and resulted on low contribution for cluster adjustments. However, the allocation model fitting for new points presented good results, though a real case assessment is still required. The regional analysis resulted in nine regions, which were heterogeneous in only two of the 117 evaluated periods. Moreover, from the KS test ( = 20%), it was verified that the regional distributions were valid for 97.8% of the series, confirming the possibility to use regional distribution, without any local scaling factor.

Made available in DSpace on 2013-10-11T13:35:22Z (GMT). No. of bitstreams: 1 000451032-Texto+Completo-0.pdf: 3224202 bytes, checksum: 0ed1399ff0656c16c4c22f4f6e16cb87 (MD5) Previous issue date: 2013
The use of critical and complex systems at automation of daily tasks increases the people’s dependence, generating unease about the safety of such systems. In the last years several techniques have been developed to facilitate activities related to design validation in the early stages of the development cycle. Model Checking is an automatic formal technique that allows verification of finite-state concurrent systems under properties described in temporal logics by employing verification algorithms that exhaustively assess the correctness of the system under consideration. Indeed, this technique is costly with respect to storage and processing, justifying the development of parallel and distributed algorithms for powerful computing clusters. This dissertation reports the study and development of verification algorithms for models described in Stochastic Automata Networks and properties written in Computation Tree Logic temporal logic for environments that address memory spaces in a distributed way.
O emprego de sistemas complexos e críticos para automação de tarefas do cotidiano faz crescer a dependência das pessoas, gerando desconforto em relação à segurança de tais sistemas. Nos últimos anos algumas técnicas têm sido desenvolvidas visando facilitar as atividades relacionadas à validação de projetos nos estágios iniciais do ciclo de desenvolvimento. Verificação de modelos é uma técnica formal automática que permite a verificação de sistemas concorrentes de estados finitos sob propriedades descritas em lógicas temporais através do emprego de algoritmos que avaliam exaustivamente o sistema sob consideração. Entretanto, esta técnica é custosa no que tange ao armazenamento em memória e processamento, justificando o desenvolvimento de algoritmos paralelos e distribuídos para poderosos agregados computacionais. Esta dissertação relata o estudo e desenvolvimento de algoritmos de verificação de modelos descritos em Redes de Autômatos Estocásticos e propriedades descritas na lógica temporal Computation Tree Logic para ambientes que endereçam espaços de memória de maneira distribuída.

Made available in DSpace on 2016-12-23T14:37:37Z (GMT). No. of bitstreams: 1 Felipe Pianna Costa.pdf: 3475348 bytes, checksum: 7fefca7d2f234254e722f1148c4e3e44 (MD5) Previous issue date: 2011-07-11
Coordenação de Aperfeiçoamento de Pessoal de Nível Superior
Nos últimos anos, vem aumentando a adoção das técnicas de agricultura de precisão (AP) em culturas anuais e perenes no Brasil. Porém, para a cafeicultura de montanha estão sendo realizadas pesquisas para adaptação de soluções tecnológicas viáveis na aplicação das técnicas de AP. O objetivo desta pesquisa foi utilizar os conceitos e métodos da análise espacial e temporal no estudo da produtividade e fertilidade do solo e desenvolver uma metodologia de classificação fuzzy para a definição de zonas de aplicação de insumos em três safras de café conilon. O trabalho foi realizado em uma área experimental cultivada com a variedade de Coffea canephora Pierre ex Froenher (ROBUSTA TROPICAL Emcaper 8151‟). Os pontos de amostragens de produtividade (sc ha-1) e atributos químicos do solo (pH, P, K, CTC e V) foram georreferenciados, compondo uma malha irregular totalizando 109 pontos. Cada ponto amostral foi composto de cinco plantas para a colheita do café, com as amostras de solo coletadas na profundidade de 0,0 0,2 m na projeção da copa do cafeeiro. Foi utilizada a análise geoestatística para interpolação dos dados, recursos de geoprocessamento para determinação do índice de produtividade e fertilidade do solo entre as safras e lógica fuzzy para análise multicritério na definição de zonas de aplicação de insumos. Nas três safras, a produtividade e os atributos químicos do solo apresentam variabilidade espacial e temporal. A análise quantitativa por meio dos mapas possibilitou observar que os níveis de produtividade e fertilidade do solo apresentam regiões com alternância de valores entre as diferentes safras. Os índices quantitativos obtidos de produtividade de -18% e -57,1% e fertilidade de 24,3% e 12,3% entre a segunda e a primeira safra e a terceira e a segunda safra, respectivamente, representam a variabilidade temporal e a distribuição espacial da produtividade e da fertilidade do solo entre as diferentes safras. A classificação fuzzy auxilia na tomada de decisão para definição de zonas de aplicação de insumos na área, revelando em maior percentual da área, notas de média aplicação de insumos de 3,4 a 6,3 nas três safras.
In recent years, the adoption of precision agriculture techniques in annual and perennial crops was increasing in Brazil. However for the coffee cultivated in mountainous regions are still being conducted research to adapt technology solutions feasible to apply these techniques. The objective of this research was to use the concepts and methods of spatial and temporal analysis in the study of soil fertility and productivity and develop a fuzzy classification methodology for defining areas of application of inputs in three conilon coffee crops. The work was developed an area of Coffea canephora Pierre ex Froenher (ROBUSTA TROPICAL Emcaper 8151‟). In the selected area an irregular grid was built, including 109 points of samplings demarcated and georeferenced. Each sample point was composed of five plants to evaluate the productivity (sc ha-1) and chemical soil attributes (pH, P, K, CTC e V) in the layer of 0-20 cm of depth in canopy‟s projection. The geostatistic analysis was applied to data interpolation, geoprocessing resources to determinate the productivity and soil fertility level and a multicriteria analysis was carried out applying fuzzy logic to definition of inputs application zones. At the three crops, the productivity and soil atributes show spatial and temporal variability. The quantitative analysis showed alternating regions of rate productivity and soil fertility values between the different crops. The quantitative levels of productivity -18% and -57.1% and fertility 24.3% and 12.3% between the second and first crop and the third and second crop, respectively, represent temporal variability and spatial distribution of the productivity and fertility between the different crops. The classification fuzzy subsidizing the decision-making process to define inputs application zones, showing in the mainly percentage of the area, medium marks of inputs application 3.4 to 6.3 on the three crops.

Submitted by Fabio Sobreira Campos da Costa (fabio.sobreira@ufpe.br) on 2017-07-12T13:26:23Z No. of bitstreams: 2 license_rdf: 811 bytes, checksum: e39d27027a6cc9cb039ad269a5db8e34 (MD5) SergioBarzaDissertation.pdf: 2147656 bytes, checksum: 5c75fe2262be1d224538c1ad6a575ebb (MD5)
Made available in DSpace on 2017-07-12T13:26:23Z (GMT). No. of bitstreams: 2 license_rdf: 811 bytes, checksum: e39d27027a6cc9cb039ad269a5db8e34 (MD5) SergioBarzaDissertation.pdf: 2147656 bytes, checksum: 5c75fe2262be1d224538c1ad6a575ebb (MD5) Previous issue date: 2016-02-25
Software Maintainability (SM) has been studied since it became one of the key componentes of the software quality model accepted around the world. Such models support researchers and practitioners to evaluate the quality level of his systems. Therefore, many researchers have proposed a lot of metrics to be used as SM indicators. On the other hand, there is a suspicious that using SM metrics on industry is different from the academic context. In this case, practitioners do not adopt the metrics proposed/used by academia. Consequently, the goal of this research is to investigate the SM metrics adoption and applicability scenario on the Brazilian industrial context. This study will allow confirming if the practitioners use the SM metrics proposed by academics around the globe or if they propose their own metrics for SM measurement. As empirical method for data assessment, we used survey, divided in two steps. The first one was focused in gathering information that allowed us to design a specific scenario about the use and applicability of SM metrics. To achieve this goal, it was chosen, as research instrument, semi-structured interviews. The next step focused in a more general scenario, compassing the Brazillian software production industrial context. An online questionnaire was used as research instrument. Practitioners with different positions in several companies participated of this work. Data from requirements engineers, quality analysts, testers, developers and project managers were collected. 7 software companies participated in the first part of the study and 68 valid answers were collected on the second moment, resulting in 31 SM metrics listed. The results showed us that about 90% of the companies perform maintenance on their software products. However, only 60% confirms using maintainability metrics, resulting in a discrepancy regarding software maintenance vs SM metrics. Nearly half of the companies researched have used well-defined processes to collect these metrics. Nevertheless, there are those that do not have any formal methodology. Instead of it, they have used SM metrics that best fit to the needs of a specific project. The conclusions of this study point to an issue that is nothing new in the academic researchers around the world. Many of the academics results conducting, mainly, in the universities, are not coming to the software industries and this fact is also a truth when the subject is software maintenance. The results of this research may lead to discussions on how SM metrics are being proposals nowadays.
Manutenibilidade de Software (MS) é estudada desde que se tornou um dos componente de modelos de qualidade aceitos globalmente. Tais modelos auxiliam pesquisadores e profissionais do mercado na avaliação do nível de qualidade dos seus sistemas. Como consequência, muitos pesquisadores vêm propondo métricas que podem ser utilizadas como indicadores de MS. Por outro lado, existe uma suspeita que o uso de métricas de MS ocorre de maneira diferente da academia. Neste caso, as empresas não estão adotando as métricas que estão sendo propostas no ambiente acadêmico. O objetivo desta pesquisa é investigar o cenário de adoção e aplicação de métricas de manutenibilidade de software sob o contexto industrial brasileiro. Este estudo permitirá afirmar se estas empresas utilizam atributos de MS propostos por acadêmicos ao redor do mundo ou se elas propõem suas próprias métricas para medição de MS. Para ter acesso aos dados desta pesquisa, foi utilizado o método empírico survey, dividido em duas etapas. A primeira etapa objetivou levantar informações que permitissem um panorama mais específico sobre a utilização e aplicação de tais métricas. Para isto, foi escolhido, como instrumento de pesquisa, entrevistas semi-estruturadas. A segunda etapa apresenta um enfoque mais amplo, englobando todo o cenário industrial de produção de software brasileira. Um questionário online foi utilizado como instrumento de pesquisa. Profissionais de diferentes posições em várias empresas participaram desta pesquisa. Foram coletados dados de engenheiros de requisitos, analista de qualidade, testadores, desenvolvedores, gerente de projetos, entre outros. Sete empresas participaram da primeira etapa da pesquisa e 68 respostas válidas foram levantadas no segundo momento. Com isto, 31 métricas de MS foram identificadas. Os resultados mostram que cerca de 90% das empresas realizam manutenção em seus produtos de software. Porém somente 60% (aproximadamente) afirmaram fazer uso de métricas de MS, resultando em uma discrepância com relação à manutenção de software vs. uso de métricas. Quase metade das empresas possuem processos bem definidos para coletar estas métricas. Entretanto, muitas delas ainda não apresentam tais processos formais de coleta. Neste último caso, elas utilizam aqueles atributos que melhor se adaptam às necessidades de um projeto específico. As conclusões deste estudo apontam para problemas que não é novidade nas pesquisas acadêmicas ao redor do mundo. Pela amostra investigada neste trabalho, reforça-se a suspeita de que muitos dos resultados das pesquisas científicas realizadas nas universidades não estão chegando na indústria e este fato se reflete quando o assunto é manutenção de software. Os resultados deste estudo apresentam dados que poderão ocasionar discussões sobre a forma como as métricas de manutenibilidade são propostas atualmente.

A evolução de sistemas de gerenciamento de tráfego aéreo é pesquisada para suportar o crescimento na demanda por transporte aéreo. Uma alternativa para essa evolução é o aumento no grau de automação. Os sistemas automatizados precisam ser tão seguros quanto os sistemas em operação atualmente. Com o uso de técnicas de especificação e verificação formal é possível avaliar os requisitos de sistemas. Neste trabalho, é proposto um ciclo de especificação formal, que consiste em um conjunto de diretrizes para aplicação de técnicas de métodos formais em requisitos escritos em linguagem natural. O resultado esperado da aplicação deste ciclo é um conjunto de requisitos escritos em linguagem natural verificados formalmente. O ciclo é composto pelas etapas: levantamento de requisitos do sistema e classificação em padrões de especificação; mapeamento dos requisitos para as linguagens de especificação formal LTL (Linear Temporal Logic) e CTL (Computation Tree Logic); verificação formal da especificação com o verificador NuSMV; ajustes na especificação baseada nos resultados da verificação; ajustes nos requisitos baseados nos ajustes na especificação. As diretrizes propostas são definidas com a análise da verificação formal do Automated Airspace Concept (AAC), padrões de especificação e diretrizes para uso do verificador NuSMV. Os resultados esperados são obtidos na aplicação do ciclo de especificação em dois estudos de caso. A principal contribuição do trabalho é o conjunto de diretrizes para elaboração de expressões escritas em linguagem de especificação formal baseadas em requisitos escritos em linguagem natural e que podem ser verificadas formalmente.
Air traffic management systems evolution is being researched to support air transportation demand growth. An evolution alternative is system automation degree increase. Automated systems need to be as safe as current operating systems. It is possible to analyze system requirements with the application of formal specification and formal verification techniques. In this work, a specification cycle is proposed. The specification cycle is a set of guidelines to use formal method techniques on requirements written in natural language. The specification cycle application expected result is a set of formally verified requirements written in natural language. This cycle is comprised of the following stages: system requirements elicitation and specification pattern classification; requirements mapping to LTL (Linear Temporal Logic) and CTL (Computation Tree Logic) formal specification languages; specification formal verification using the NuSMV verifier; formal specification adjustment based on verification results; requirements adjustment based on formal specification adjustment. The proposed guidelines are defined with the Automated Airspace Concept (AAC) formal verification analysis, specification patterns and guidelines for the NuSMV formal verifier use. The expected results are accomplished in the specification cycle application on two study cases. The main contribution of this work is the set of guidelines applied to formulate formally verifiable expressions specified in formal specification languages based on system requirements written in natural language.

Submitted by José sobreiro filho (sobreirounesp@gmail.com) on 2016-09-20T16:55:23Z No. of bitstreams: 1 TESE_SOBREIRO_190916.pdf: 14156754 bytes, checksum: 42d2893bd28b01c852ada1a0c64f2158 (MD5)
Approved for entry into archive by Ana Paula Grisoto (grisotoana@reitoria.unesp.br) on 2016-09-20T18:42:51Z (GMT) No. of bitstreams: 1 sobreirofilho_j_dr_prud.pdf: 14156754 bytes, checksum: 42d2893bd28b01c852ada1a0c64f2158 (MD5)
Made available in DSpace on 2016-09-20T18:42:51Z (GMT). No. of bitstreams: 1 sobreirofilho_j_dr_prud.pdf: 14156754 bytes, checksum: 42d2893bd28b01c852ada1a0c64f2158 (MD5) Previous issue date: 2016-09-16
Fundação de Amparo à Pesquisa do Estado de São Paulo (FAPESP)
Neste trabalho, apresentamos um conjunto de reflexões cujo objetivo é de contribuir para a construção de uma teoria geográfica sobre movimentos socioespaciais e contentious politics. Assim, partimos dos principais conceitos geográficos (espaço, território, rede, lugar e escala) e das reflexões sobre movimentos socioespaciais e socioterritoriais, contentious politics, socio-spatial posicionality, convergence space e terrains of resistance, bem como da teoria da produção do espaço, para apresentar um modelo explicativo eminentemente geográfico. Tempo e espaço apresentam-se indissociáveis desde o remontar histórico dos conflitos até a própria análise dos conflitos contemporâneos. Por fim, o desfecho deste trabalho tem a nossa contribuição teórica, denominada por lógica-racionalidade espaço-temporal, lastreada na análise movimentos socioespaciais e casos de contentious politics no Brasil e Argentina.
In this thesis, we present a set of reflections whose objective is to contribute to the construction of a geographical theory of socio-spatial movements and contentious politics. Hence we set out and use the key geographical concepts (space, territory, network, place and scale) and reflections on socio-spatial and socio-territorial movements, contentious politics, socio-spatial positionality, convergence space and terrains of resistance, as well as the theory of production of space to present an eminently geographic explanatory model. Time and space are presented as inseparable from the history of the conflict as well in the analysis of contemporary conflicts. Finally, the outcome of this work is our theoretical contribution, called spatial-time logic-rationality, based in the analysis of the socio-spatial movements and cases of contentious politics in Brazil and Argentina.
FAPESP: 2013/22180-0

Orientador: Bernardo Mançano Fernandes
Banca: Carlos Alberto Feliciano
Banca: Facundo Martin Garcia
Banca: Marco Antonio Mitidiero Júnior
Banca: Djoni Roos
Resumo: Neste trabalho, apresentamos um conjunto de reflexões cujo objetivo é de contribuir para a construção de uma teoria geográfica sobre movimentos socioespaciais e contentious politics. Assim, partimos dos principais conceitos geográficos (espaço, território, rede, lugar e escala) e das reflexões sobre movimentos socioespaciais e socioterritoriais, contentious politics, socio-spatial posicionality, convergence space e terrains of resistance, bem como da teoria da produção do espaço, para apresentar um modelo explicativo eminentemente geográfico. Tempo e espaço apresentam-se indissociáveis desde o remontar histórico dos conflitos até a própria análise dos conflitos contemporâneos. Por fim, o desfecho deste trabalho tem a nossa contribuição teórica, denominada por lógica-racionalidade espaço-temporal, lastreada na análise movimentos socioespaciais e casos de contentious politics no Brasil e Argentina.
Abstract: In this thesis, we present a set of reflections whose objective is to contribute to the construction of a geographical theory of socio-spatial movements and contentious politics. Hence we set out and use the key geographical concepts (space, territory, network, place and scale) and reflections on socio-spatial and socio-territorial movements, contentious politics, socio-spatial positionality, convergence space and terrains of resistance, as well as the theory of production of space to present an eminently geographic explanatory model. Time and space are presented as inseparable from the history of the conflict as well in the analysis of contemporary conflicts. Finally, the outcome of this work is our theoretical contribution, called spatial-time logic-rationality, based in the analysis of the socio-spatial movements and cases of contentious politics in Brazil and Argentina
Doutor

Dissertação (mestrado)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Ciência da Computação, Mestrado em Informática, 2015.
Submitted by Albânia Cézar de Melo (albania@bce.unb.br) on 2015-03-31T15:40:32Z No. of bitstreams: 1 2015_ThiagoCoelhoVieira.pdf: 662085 bytes, checksum: 8fae3df1c74c85937e5cd8c48823b60b (MD5)
Approved for entry into archive by Ruthléa Nascimento(ruthleanascimento@bce.unb.br) on 2015-04-20T19:01:54Z (GMT) No. of bitstreams: 1 2015_ThiagoCoelhoVieira.pdf: 662085 bytes, checksum: 8fae3df1c74c85937e5cd8c48823b60b (MD5)
Made available in DSpace on 2015-04-20T19:01:54Z (GMT). No. of bitstreams: 1 2015_ThiagoCoelhoVieira.pdf: 662085 bytes, checksum: 8fae3df1c74c85937e5cd8c48823b60b (MD5)
Diversos tipos de lógicas são usadas como linguagens para descrever sistemas complexos e suas propriedades com a finalidade de serem verificadas formalmente. Provadores de teoremas baseados em tableaux são ferramentas computacionais capazes de realizar esta tarefa de verificação. Em (WDF98) é proposto um método de prova baseado em tableaux para duas lógicas epistêmico-temporais, KL(n) e BL(n). Neste trabalho implementamos o método de prova baseado em tableaux descrito em (WDF98) e apresentamos um algoritmo para verificação de propriedades epistêmicas e temporais sobre a estrutura do tableau construída por este método.
Logics are used as languages to describe complex systems and their properties in order to be formally verified. Tableaux-based theorem-provers are computational tools which can be used to perform this verification task. (WDF98) propose a proof method based on tableaux for both the epistemic-temporal logics KL(n) and BL(n) . In this work we implement the tableaux-based proof method described in (WDF98) and present an algorithm for verification of epistemic-temporal properties over the structure of the tableau built by this method.

Submitted by Johnny Rodrigues (johnnyrodrigues@ufcg.edu.br) on 2018-08-22T19:52:23Z No. of bitstreams: 1 ANA EMÍLIA VICTOR BARBOSA - DISSERTAÇÃO PPGCC 2007..pdf: 1669761 bytes, checksum: f47054507fe9200c8d1d56d2848ae276 (MD5)
Made available in DSpace on 2018-08-22T19:52:23Z (GMT). No. of bitstreams: 1 ANA EMÍLIA VICTOR BARBOSA - DISSERTAÇÃO PPGCC 2007..pdf: 1669761 bytes, checksum: f47054507fe9200c8d1d56d2848ae276 (MD5) Previous issue date: 2007-04-20
Capes
Neste trabalho propomos uma técnica que visa detectar violações de propriedades comportamentais automaticamente durante a execução de sistema de software concorrentes. A técnica foi inspirada na metodologia de desenvolvimento Design by Contract (DbC). DbC permite que os desenvolvedores adicionem aos programas asserções para que sejam verificadas em tempo de execução. O uso de asserções para expressar propriedades de programas concorrentes (multithreaded)eparalelos, entretanto,não ésuficiente. Nesses sistemas,muitas das propriedades comportamentais de interesse, como vivacidade e segurança, não podem ser expressas apenas com asserções. Essas propriedades requerem o uso de operadores temporais. Neste trabalho, utilizamos Lógica Linear Temporal (Linear Time Logic - LTL) para expressar o comportamento desejado. Para dar suporte a checagem do comportamento dos programas em tempo de execução, propomos uma técnica baseada em Programação Orientada a Aspectos, que permite que o programa seja continuamente monitorado (o comportamento é checado através do uso de autômatos que permite a deteção de comportamentos inesperados). Associada a cada propriedade comportamental existe um conjunto de pontos de interesse do código-fonte que devem obedece-la. Esses pontos são então monitorados durante a execução do sistema através do uso de aspectos. Entre outros benefícios, a técnica permite que o sistema de software alvo seja instrumentado de maneira não intrusiva, sem alterar o código-fonte — particulamente, nenhum código do software alvo deve ser modificado para execução da monitoração. Para validar este trabalho, desenvolvemos como prova de conceitos um protótipo que implementa a técnica e permite a monitoração de programas Java multi-threaded, chamado DesignMonitor. Essa ferramenta é apresentada e discutida através de um estudo de caso para demonstrar a aplicação da técnica
In this work we propose and develop a technique that allows to detect the violation of behavior properties of concurrent systems. The technique was inspired by the Design by Contract (DbC) programming methodology, which proposes the use of assertions and their evaluation at runtime to check programs behavior. The use of simple assertions to express properties of concurrent and parallel programs, however, is not sufficient. Many of the relevant properties of those systems,s uch as liveness and security, can not be expressed with simple assertions. Thesepropertiesrequiretheuseof temporal operators. In our work, we used Linear Time Logic (LTL) to specify the expected behavior. To support the runtime checking of the program against the expected behavior, we propose a technique, based on Aspect-Oriented Programming, that allows the program to be continuously monitored (behavior is checked against automata that allows the detection of unexpected behaviors). Each property is mapped to a set of points of interest in the target program. Those points are then monitored during the system execution through aspects. Among other benefits, the technique allows the instrumentation of the target software to be performed automatically and in a non-intrusive way — in particular, no code must be changed toturn monitoring on or off. To validate the work, we developed a proof of concept prototype tool that implements the technique and allows the monitoring of multi-threaded Java programs, called DesignMonitor. The tool was used in case study that has allowed the evaluation and the discussion of practical issues related with the technique.

Esta dissertação tem como objetivo a aplicação de sistemas com arquitetura neuro-fuzzy na predição de funções que geram séries temporais. A arquitetura pesquisada é a Adaptive Neuro-Fuzzy Inference System (ANFIS). Esta arquitetura se trata de um Fuzzy Inference Systems (FIS) im- plementado sob o paradigma das redes neurais artificiais. Ao fazer o uso da tecnologia de redes neurais artificiais, o ANFIS possui a capacidade de apren- dizagem dos dados do ambiente no qual está inserido. Da mesma forma, por implementar um FIS, o ANFIS agrega também a competência de processamento linguístico. Logo, o ANFIS pode ser categorizado como um sistema híbrido. Ao longo dos capítulos estão expostos alguns conceitos e fundamentos da Teoria Fuzzy, assim como das redes neurais artificiais e sistemas híbridos. Ao final do trabalho são realizadas algumas discussões, análises e conclusões, as quais permitem a possibilidade de futuras aplicações e extensão deste.
This master dissertation has as main objetive applies systems of neuro-fuzzy architecture for functions prediction in serie times. The architecture carried out is the Adaptive Neuro-Fuzzy Inference System (ANFIS). This architecture is a kind of Fuzzy Inference Systems (FIS) implemen- tation under a paradigm of arti¯cial neural networks. Making use of technology of arti¯cial neural networks, the ANFIS has the capacity of learning with environ- ment data that inserted on. As the same, the ANFIS had been implemented to be a FIS. Then it can process simbolic variables. So, an ANFIS can be described like a hibrid system. All over the chapters are showed some concepts and fundaments of Fuzzy theory, arti¯cial neural networks and hidrid systems. The purpose of the tests the ANFIS, it were been made from a logistic function and a Mackey-Glass function. This tests were against with an estimation function made by MLP net. At the end of the work are some discussions, analyses and conclusions that allows futures possibilites of applications and extensions of this work.

Essa pesquisa consiste emsistematizar, analisar e interpretar informações e dados capazes de integrar uma discussão teórico-empírica sobre as feiras e congressos médicos como círculos de cooperação no espaço do complexo industrial da saúde no Brasil. Para tanto propomos analisar o papel da proximidade geográfica temporária no período técnicocientífico informacional a fim de compreender as possíveis funções dessas densidades comunicacionais temporárias no atual contexto de fragmentação geográfica da produção, internacionalização da economia e ampla necessidade de circulação de informações e conhecimentos. Nesse sentido, a análise das feiras e congressos médicos associados a análise das transformações do conteúdo do espaço geográfico da formação socioespacial brasileira e do desenvolvimento do complexo industrial da saúde no Brasil permitiu compreendê-los como elementos que sustentam os atuais círculos de cooperação ao imbricarem o nível local e global do acontecer, constituindo o acontecer efêmero de uma solidariedade globalizada através da divisão internacional do trabalho.
This research consists in the organization, analysis and interpretation of information and data enough to sufficiently compose a theoretical and empirical framework about medical trade fairs and medical congresses as circles of cooperation in in space. As to follows the analysis of the current role of temporary geographical proximity in the technical-scientific and informational period in order to comprehend the possible roles of these temporary communicational densities in the current context of geographical fragmentation of production, economic internationalization, and the widespread need of information and knowledge circulation. In this sense, the study of medical trade fairs and medical congresses related to the study of the transformation of Brazil\'s geographical space intertwined with the study of the development of the Brazilian health industrial complex allowed us to understand those two phenomena as elements that sustain the contemporary circles of cooperation, by overlapping local and global and constituting ephemeral gathering of a globalized solidarity made possible through the international division of labor

Nessa dissertação, abordamos o problema de dois qubits interagindo com campos externos e entre si controladamente, de acordo com um Hamiltoniano considerado realista para implementação da porta lógica quântica XOR. Introduzimos acoplamentos entre as observáveis do sistema de dois qubits e um banho de osciladores harmônicos a fim de tratarmos o problema da dissipação e da decoerência. Primeiramente nós consideramos o limite no qual a decoerência é mais rápida que qualquer processo gerado pelo Hamiltoniano do sistema. Prosseguimos então, através do método numérico conhecido como Integrador Unitário, com o estudo da matriz densidade do sistema durante a operação da porta lógica quântica sem incluir, inicialmente, o acoplamento com o banho de osciladores harmônicos. Finalmente, implementamos o método numérico conhecido como Propagador quase adiabático para estudar a decoerência e a dissipação durante a operação da porta lógica quântica XOR, a fim de analisarmos os aspectos perturbativos do sistema quântico de dois qubits.
In this dissertation, we approach the problem of two qubits interading with themselves and with externa1 fields in a controlled way, according to a Hamiltonian considered realistic to implement the XOR quantum gate. We introduce couplings between the observables of the two-qubits system and of a bath of harmonic oscillators, to treat the problems of dissipation and decoherence. Preliminarly, we consider the limit in which decoherence is faster than any process dictated by the Hamiltonian evolution of the system. Then, through a unitary-integrator numerical method, we proceed with the study of the evolution of the density matrix of the system during the operation of the logical quantum gate, initially, without the coupling with the bath of harmonic oscillators. Finally, we use the quasiadiabatic path integral method to study the dissipation and decoherence during the logical operation, through the inclusion of the bath.

Dissertação (mestrado) - Pontifícia Universidade Católica do Paraná, Curitiba, 2007
Bibliografia: f. 109-121
A modelagem de sistemas dinâmicos não-lineares que usam sistemas nebulosos tem sido cada vez mais reconhecida como um paradigma da previsão de séries temporais. Modelar um sistema por meio de um sistema nebuloso engloba um conjunto de regras nebulosas e d
The modeling of nonlinear dynamical systems that uses fuzzy systems has been increasingly recognized as paradigm of time series forecast. Modeling a system through a fuzzy system comprises a set of fuzzy rules and membership functions. In this dissertatio

Submitted by Luiza Maria Pereira de Oliveira (luiza.oliveira@ufpe.br) on 2017-07-20T17:58:36Z No. of bitstreams: 2 license_rdf: 811 bytes, checksum: e39d27027a6cc9cb039ad269a5db8e34 (MD5) Dissertacao_Hugo_Gouveia_Biblioteca_Central (1).pdf: 2697951 bytes, checksum: c6c11f656ee81de84aeda051d25620c4 (MD5)
Made available in DSpace on 2017-07-20T17:58:36Z (GMT). No. of bitstreams: 2 license_rdf: 811 bytes, checksum: e39d27027a6cc9cb039ad269a5db8e34 (MD5) Dissertacao_Hugo_Gouveia_Biblioteca_Central (1).pdf: 2697951 bytes, checksum: c6c11f656ee81de84aeda051d25620c4 (MD5) Previous issue date: 2011-12-22
A previsão de ventos é de extrema importância para auxiliar nos estudos de planejamento e programação da operação da geração eólica. Vários estudos já comprovaram que o potencial eólico brasileiro, principalmente no Nordeste, onde os ventos apresentam uma importante característica de complementaridade em relação às vazões do rio São Francisco, pode contribuir significativamente para o suprimento de energia elétrica. Entretanto, o uso das forças dos ventos para produção de energia elétrica produz alguns inconvenientes, tais como, incertezas na geração e a dificuldade no planejamento e operação do sistema elétrico. Este trabalho propõe e desenvolve modelos de previsões de velocidades médias horárias de ventos e geração eólica a partir de técnicas de Redes Neurais Artificiais, Lógica Fuzzy e Análise Wavelet. Os modelos foram ajustados para realizar previsões com passos variáveis de até vinte e quatro horas. Para as previsões realizadas com alguns dos modelos desenvolvidos, os ganhos em relação aos modelos de referência foram da ordem de 80% para as previsões com passo de uma hora. Os resultados demonstraram que a Análise Wavelet aliada às ferramentas de inteligência artificial fornecem previsões muito mais confiáveis do que aquelas obtidas com os modelos de referência, principalmente para as previsões com passos de 1 – 6 horas.
Wind forecasting is extremely important to assist in planning and programming studies for the operation of wind power generation. Several studies have shown that the Brazilian wind potential can contribute significantly to the supply of electricity, especially in the Northeast, where the winds have an important feature of complementarity in relation to the flows of the San Francisco River. However, the use of of wind to generate electricity has some drawbacks, such as uncertainties in generation and some difficulty in planning and operation of the power system. This work proposes and develops models to forecast hourly average wind speeds and wind power generation based on techniques of Artificial Neural Networks, Fuzzy Logic and Wavelets. The models were adjusted for forecasting with variable steps up to twenty-four hours ahead. The gain of some models developed in relation to the reference models were approximately 80% for forecasts in a period of one hour ahead. The results showed that the wavelet analysis combined with artificial intelligence tools provide forecasts more reliable than those obtained with the reference models, especially for forecasts in a period of 1 to 6 hours ahead.

Submitted by Kelren Mota (kelrenlima@ufpa.br) on 2018-06-15T19:50:31Z No. of bitstreams: 2 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Dissertacao_PrevisãoDemandaEnergia.pdf: 5554955 bytes, checksum: 421efd02a7332d22d5cbcb98ca169611 (MD5)
Approved for entry into archive by Kelren Mota (kelrenlima@ufpa.br) on 2018-06-15T19:50:59Z (GMT) No. of bitstreams: 2 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Dissertacao_PrevisãoDemandaEnergia.pdf: 5554955 bytes, checksum: 421efd02a7332d22d5cbcb98ca169611 (MD5)
Made available in DSpace on 2018-06-15T19:50:59Z (GMT). No. of bitstreams: 2 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Dissertacao_PrevisãoDemandaEnergia.pdf: 5554955 bytes, checksum: 421efd02a7332d22d5cbcb98ca169611 (MD5) Previous issue date: 2018-04-12
O estudo da previsão de demanda correlato a séries temporais de energia elétrica desenvolve um processo de otimização para o atendimento de energia elétrica, com o objetivo de aprimorar a rotina de previsão. No presente trabalho, é apresentada uma comparação de três modelos autorregressivos utilizados para a otimização mencionada, com o modelo de lógica fuzzy, dimensionado por meio da função de autocorrelação estendida. Os dados de consumo de energia elétrica presentam uma estrutura de série temporal sazonal, suscitando um recorte histórico com as características de consumo de energia elétrica do Estado de Rondônia, e neste objeto foi implementada uma metodologia de previsão por meio de modelos já sedimentados e em comparativo a um novo modelo, apresentado em Métodos de Identificação Fuzzy Para Modelos Autorregressivos Sazonais Mediante a Função de Autocorrelação Estendida. Analisa-se, então, as performances dos modelos e aplicação para previsão de demanda de energia elétrica a curto prazo, 5 (cinco) dias úteis da semana, para fins de contratação de pacotes de energia elétrica junto as concessionárias distribuidoras de energia elétrica, obedecendo a legislação vigente sobre leilões e contratos de compra. No decorrer do trabalho, foram analisados os resultados de previsão de energia elétrica, pelos modelos apresentados, o modelo proposto em Sistema Fuzzy relacionado a Autocorrelação Estendida, sendo o mais satisfatório confirmado por erros de previsão em relação a demanda de energia elétrica para o Estado de Rondônia, e atendendo legislação sobre previsão e demanda de energia elétrica no Brasil. Palavras-chave: Demanda de Energia Elétrica, Séries Temporais Fuzzy, Função de Autocorrelação Estendida, Previsão de Energia Elétrica em curto Prazo.
The study of demand forecast correlated to time series of electric energy develops an optimization process for the supply of electricity, with the objective of improving the forecasting routine. In this study, it is presented a comparison of three autoregressive models used for the mentioned optimization, with the fuzzy logic model, dimensioned through the extended autocorrelation function. The electric energy consumption data presents a seasonal time series structure, provoking a historical cut with the electric power consumption characteristics of the State of Rondônia, and in this object was implemented a methodology of prediction by means of already sedimented models and in comparison to a new model, presented in Fuzzy Identification Methods for Autoregressive Models Using the Extended Autocorrelation Function. The performance of the models and application for short-term electricity demand forecasting, 5 (five) five business days of the week, was analyzed for the purpose of contracting electric energy packages with the electricity distribution concessionaires, in compliance with the legislation current agreement on auctions and purchase agreements. In the course of the work, we analyzed the results of electric energy prediction, by the models presented, the proposed model in Fuzzy System related to Extended Autocorrelation, being the most satisfactory one confirmed by errors of forecast in relation to the demand of electric power for the State of Rondônia, and complying with legislation on forecasting and demand of electric energy in Brazil.

O mercado automotivo brasileiro anual apresenta comportamento instável e de difícil compreensão a curto prazo, apesar da tendência de crescimento. A fim de entender melhor tal comportamento, este trabalho propõe: i) Estudar um modelo de série temporal adequado ao mercado ii) Criar um modelo de transferência com as variáveis que influenciam o mercado iii) Utilizar modelos de inteligência artificial de lógica nebulosa (fuzzy), iv) Comparar os diversos modelos e seus erros e v) Fazer previsões do mercado ate 2010. Para o modelo de série temporal, concluímos que se trata de um modelo ARIMA (1,1,0). Porém, ao se retirar o termo não-estacionário, os dados se tornaram um ruído branco sem relação com o tempo (ano). Então, o modelo autoregressivo foi usado. Para o estudo de função de transferência, concluímos que as variáveis significativas encontradas para o modelo de transferência foram somente PIB brasileiro e renda média dentre as estudadas (Juros, Câmbio, Inflação IGP, Salário Mínimo, Renda média, PEA, Exportação, Balança comercial, Preço do Petróleo, Carga tributária população, PIB Brasileiro, PIB Mundial). Utilizou-se dois modelos de inteligência artificial neuro-fuzzy: um simples, com o ano como entrada, e outro complexo, que usa como entrada valores anteriores do mercado. No comparativo, para a amostra de 1957 a 2004 o modelo que representa o mercado com menor soma dos quadrados dos erros é o modelo neuro-fuzzy. Para a amostra de 1977 a 2004 é o modelo de função de transferência. A previsão para 2010 obteve valore entre 1,6 e 1,8 milhões para a amostra de 48 pontos e 1,3 e 2,4 milhões para a amostra de 28 pontos. Vale a pena ressaltar que este modelo não apresentou muita diferença do que vem prevendo a indústria usando um modelo simplista de regressão simples.

MENEZES, José Wally Mendonça. Análise de performance de sólitons ópticos espaço-temporais em guia planar com não-linearidade cúbico quintica periodicamente modulada e circuitos lógicos operando nos regimes Kerr instantâneo e relaxado. 2010. 149 f. Tese (Doutorado em Física) - Programa de Pós-Graduação em Física, Departamento de Física, Centro de Ciências, Universidade Federal do Ceará, Fortaleza, 2010.
Submitted by francisco lima (admir@ufc.br) on 2014-06-30T18:38:52Z No. of bitstreams: 1 2010_tese_jwmmenezes.pdf: 7446687 bytes, checksum: 708020e7c4ad24658a46a55f2af5ebc6 (MD5)
Approved for entry into archive by Edvander Pires(edvanderpires@gmail.com) on 2014-08-06T20:53:00Z (GMT) No. of bitstreams: 1 2010_tese_jwmmenezes.pdf: 7446687 bytes, checksum: 708020e7c4ad24658a46a55f2af5ebc6 (MD5)
Made available in DSpace on 2014-08-06T20:53:00Z (GMT). No. of bitstreams: 1 2010_tese_jwmmenezes.pdf: 7446687 bytes, checksum: 708020e7c4ad24658a46a55f2af5ebc6 (MD5) Previous issue date: 2010
In this work, the propagation and stability of spatiotemporal optical solitons (or optical bullets) in a planar waveguide with periodically modulated cubic-quintic nonlinearity is presented numerically as a function of the amplitudes of modulation , the frequency of modulation and the propagation distance .With the objective of ensure the stability and preventing the collapse or the spreading of pulses, in this study we explore the cubic-quintic nonlinearity with the optical fields coupled by XPM (Cross-Phase Modulation) and take into account several values for the nonlinear parameter , for amplitudes and frequency of modulation as a function of the propagation distance , we cause the collisions of two pulses (envelope of the optical field) to ensure that the optical pulse are sólitons and, after numerical analysis was possible shown the existence of stable spatiotemporal optical sóliton. We also have presented the numerical analysis of the three-core nonlinear fiber coupler in a symmetrical planar structure and operating with instantaneous and relaxed Kerr model for generation of the all-optical logic gates. To implement this optical circuit, we used a control pulse CP with a phase difference between the inputs “I1” and “I2” of the fiber coupler and were analyzed the transmission characteristics, the Extinction Ratio as a function of the phase difference, the length normalized (LN), the figure-of-merit of the logic gates (FOMELG (dB) and the pulse evolution along the fiber coupler and, thus, ensure were demonstrated the possibilities for generating of the all-optical logic gates.
Neste trabalho, a propagação e estabilidade de sólitons espaço-temporais (ou sólitons balas) em um guia de onda planar com não linearidade cúbico quintica periodicamente modulada é apresentada em função da amplitude de modulação , da freqüência de modulação e da distância de propagação . Com o objetivo de garantir a estabilidade e prevenir o colapso ou o espalhamento dos pulsos, exploramos a não-linearidade cúbico quintica com os campos ópticos acoplados por XPM (Modulação de Fase Cruzada) e utilizando diversos valores para o parâmetro não-linear , para as amplitudes e freqüências de modulação em função da distância de propagação , provocamos a colisão de dois pulsos (campos ópticos) para garantir que estes sejam realmente sólitons e, após estas análises numéricas, foi possível mostrar a existência de sólitons espaço-temporais estáveis. Apresentamos, também, a análise numérica de um acoplador triplo não linear de fibras ópticas em uma estrutura planar simétrica e operando com o modelo Kerr instantâneo e relaxado para geração de portas lógicas ópticas. Para implementar estes circuitos, usamos um pulso de controle CP com uma diferença de fase entre as entradas “I1” e “I2” do acoplador e analisamos as características de transmissão, taxa de extinção em função da diferença de fase, a largura normalizada (LN), a figura de mérito para portas lógicas FOMELG(dB) e a evolução dos pulsos ao longo do acoplador e, assim, foi demonstrado as possibilidades para geração das portas lógicas ópticas.

Los sistemas de prueba etiquetados han sido propuestos por Gabbay como un marco unificador a través de la teoría de prueba con el fin de proporcionar sistemas de prueba para una amplia gama de lógicas. Para las lógicas modales, un ejemplo de ello son, por ejemplo, los sistemas de deducción natural etiquetados y sistemas de secuentes etiquetados, tales como los introducidos por Simpson y Negri. Estos formalismos hacen uso explícito no sólo de las etiquetas, sino también de los átomos relacionales que se refieren a la relación de accesibilidad de un modelo de Kripke. El objetivo principal de este trabajo final de Licenciatura, es poder proponer un sistema de prueba etiquetado para una Lógica Modal Intuicionista, que represente tanto la relación de accesibilidad (para la lógica modal) como la relación de preorden (para la lógica intuicionista), utilizando todo el poder de la semántica bi-relacional para las lógicas modales intuicionistas.

A presente dissertação procura estudar uma das possíveis deslocações aquando a velhice: passar a frequentar uma instituição de cuidados formais. Tendo como fundamento empírico as dinâmicas e as rotinas do Centro Social e Paroquial Nossa Senhora do Cabo, analiso as experiências típicas do envelhecimento nesta instituição, e como estas podem tanto ser desiguais como semelhantes. Partindo de observações, entrevistas e conversas, com os utentes, com as funcionárias, e, principalmente, com as auxiliares de ação direta, infiro e investigo acerca das circunstâncias que potenciam a necessidade de suporte institucional, e os diferentes suportes necessários. Considero as complexas relações entre as dimensões biológicas e as dimensões sociais do envelhecimento, e como o corpo envelhecido sugere mudanças em noções como capacidade e saúde. E, finalmente, pondero sobre o papel da passagem mecânica do tempo na condução de cada um para a velhice: uma situação incerta e inevitável, que irá preceder a morte.
The following dissertation seeks the study one of the possible dislocations in old age: to attend a formal care institution. Having as empirical foundation the dynamics and routines of the Centro Social e Paroquial Nossa Senhora do Cabo, I analyze the typical experiences of aging in this institution, and how these can be both unequal and similar. Beginning from observations, interviews and conversations, with the elderly, the employees, and, mainly, direct action assistants, I investigate the circumstances that enhance the need for institutional support, and the different necessary supports. I consider the complex relationships between the biological dimensions and the social dimensions of aging, and how the aged body suggests changes in notions such as capacity and health. And finally, I ponder the role of the mechanical passage of time in the conveyance of each to old age: an uncertain and inevitable situation, which will precede death.

Dissertação de mestrado em Engenharia de Informática
O rápido crescimento da complexidade dos sistemas de software exige, agora mais do que nunca, uma validação rigorosa dos mesmos por forma a manter ou até mesmo aumentar a confiança nestes sistemas. Em particular nos sistemas críticos, onde as falhas podem ter consequências catastróficas podendo até incluir a perca de várias vidas humanas, é de externa importância o desenvolvimento de técnicas capazes de garantir altos níveis de confiança para estes sistemas. Nesta tese é proposta a utilização de uma técnica formal para a verificação de programas Ada, que pretende aumentar a confiança em sistemas cuja implementação seja realizada nesta linguagem de programação. Mais precisamente, pretende-se a aplicação da técnica de verificação de modelos para a análise do código fonte de programas concorrentes Ada, com especial foco para o domínio dos sistemas críticos. A verificação de modelos é uma técnica bem-sucedida no que diz respeito à garantia de um aumento de fiabilidade destes sistemas. No entanto, a aplicação desta técnica a sistemas de software enfrenta ainda vários obstáculos, e as ferramentas e técnicas para ajudar a ultrapassar estes obstáculos estão ainda a ser desenvolvidas. A ferramenta desenvolvida no contexto desta tese (ATOS) visa responder a problemas como (i) a construção de modelos a partir de programas e (ii) a especificação de propriedades para estes modelos de acordo com as pretendidas para os programas. A construção manual de modelos que simulam o comportamento de programas é um processo complexo, temporalmente dispendioso, e sujeito a falhas devido à complexidade destes sistemas. De forma a ultrapassar este problema o ATOS propõe a extração automática de modelos a partir de programas Ada. Por outro lado, o mapeamento das propriedades desejadas dos programas em propriedades dos modelos pode ser urna tarefa com um grau de complexidade elevado, pois requer entre outros a utilização de um formalismo logico ao qual a maioria dos programadores não está acostumada. 0 ATOS ajuda no mapeamento destas propriedades, oferecendo vários mecanismos de suporte à sua especificação.
The rapid growth of the complexity of software systems demands, flow more than ever, a rigorous validation of these systems in order to maintain or even increase their reliability. In particular in high-integrity systems, where failures may have catastrophic consequences which may even include the lost of human lives, the development of verification techniques capable of ensuring high degrees of confidence is seen as extremely important. In this thesis the use of a formal technique for the verification of Ada programs is proposed, which aims to increase the reliability of systems whose implementation is based on this programming language. More precisely, we target the application of the model checking technique to the verification of source code of concurrent Ada programs, with a special focus on the critical systems domain. Model checking is a well-succeeded technique for providing increased levels of assurance regarding system correctness. However, its application to software systems still faces several obstacles, and the necessary tools and techniques to help in the overcoming of these problems are still being developed. The tool presented in this thesis (ATOS) addresses the problems of (i) constructing models from programs and (ii) specifying properties for models corresponding to the ones desired for programs. The manual construction of models that simulate the behavior of programs is a time-costly, complex and error-prone process, due to the complexity of these systems. In order to overcome this problem, ATOS proposes the automatic extraction of models from Ada programs. On the other hand, the mapping of the desired properties from programs to models can be a task of high complexity, because it requires among others that they are expressed in a logical formalism that most programmers are not acquainted with. ATOS helps in this mapping task by providing several mechanisms aiming to support the specification of properties.

Tesis (Lic. en Ciencias de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía, Física y Computación, 2019.
Los lenguajes modales son lenguajes adecuados para describir propiedades de grafos dirigidos con nodos etiquetados. Estas estructuras aparecen en una gran variedad de problemas de diversas áreas del conocimiento. Como consecuencia de esto, existe una gran variedad de lógicas modales. En la práctica cada vez que se define una nueva lógica modal, muchos teoremas deben ser demostrados y revisados nuevamente para esta nueva lógica. Este proceso, además de resultar tedioso, es propenso a errores. Afortunadamente, la tarea de realizar demostraciones complejas ha comenzado cada vez más a ser asistida por herramientas computacionales. En este trabajo, formalizamos y verificamos en el asistente de demostraciones Coq un teorema de invarianza bajo bisimulación de ciertas lógicas modales con operadores dinámicos capaces de modificar la relación de accesibilidad.
Modal languages are adequate languages to describe properties of labelled directed graphs. These structures appear in a wide variety of problems from different areas of knowledge. As a consequence, there exist a great number of modal logics. In practice, every time a new modal logic is defined, many theorems must be proved and peer-reviewed again for this new logic. This process, besides being tedious, is error-prone. Fortunately, the task of writing complex proofs has increasingly begun to be assisted by computational tools. In this work, we formalize and verify an invariance under bisimulation result in the proof assistant Coq for a particular family of dynamic modal logics that change the accessibility relation of a model.
Fil: Trucco, Francisco Carlos. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía, Física y Computación; Argentina.

Tesis (Doctor en Ciencias de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía, Física y Computación, 2020.
En la actualidad la tolerancia a fallas cada vez adquiere mayor importancia, debido a que cada día hay más sistemas críticos en donde es necesario garantizar cierto comportamiento deseado aún ante la ocurrencia ocasional de fallas. En este trabajo presentamos algunos formalismos lógicos que resultan adecuados para la especificación, y luego la verificación, de propiedades de sistemas tolerantes a fallas. En particular, nos enfocamos en el uso de aquellos que si bien, tradicionalmente fueron utilizados para representar y analizar la estructura lógica de normas o leyes (conocidos con el nombre de lógicas deónticas), nos posibilitan, a diferencia de otros enfoques, distinguir entre los comportamientos normal y anormal de un sistema. Hacia el final de esta tesis, además, se presentan algunas incursiones en el área de sistemas probabilistas, ya que cuando se piensa en sistemas tolerantes a fallas surge naturalmente pensar en un grado de tolerancia/robustez deseado o esperado; y es justamente este tipo de noción cuantificable la que conduce a la idea de utilizar las probabilidades para capturar este concepto. En particular se presentan algunos ejemplos para ilustrar la capacidad de dichos formalismos para capturar nociones relacionadas con tolerancia a fallas.
At present, fault tolerance is becoming more and more important, because every day there are more critical systems where it's necessary to guarantee a certain desired behavior even in the event of occasional failure. In this work we present some logical formalisms suitable for the specification, and later verification, of properties for fault tolerant systems. In particular, we focus on the use of those formalisms traditionally used to represent and analyze the logical structure of norms or laws (known as deontic logics), that allow us to distinguish between normal and abnormal behaviors of a system. Towards the end of this thesis, some forays made into the area of probabilistic systems are also presented, due that when thinking about fault tolerant systems it naturally arises the notion of a desired or expected degree of tolerance / robustness; and it's precisely this kind of quantifiable notion that leads us to think about using probabilities to capture this concept. In particular we show some examples to illustrate the ability of such formalisms to capture notions related to fault tolerance.
Fil: Kilmurray, Cecilia Noelia. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía, Física y Computación; Argentina.