Belief Revision addresses the problem of how to change epistemic states, usually represented in the literature by sets of logical sentences. Solid theoretical results were consolidated with the AGM paradigm, which deals with theories (logically closed sets of sentences). After that, the theory was extended to belief bases, that is, arbitrary sets of sentences. Besides all this theoretical framework, AI researchers face serious difficulties when trying to implement belief revision systems. One of the major complications is the closure required by AGM theory, which cannot be easily computed. Even belief bases, which do not require closure, seem to be improper for practical purposes, since their changes are usually very rigid (syntax dependent). Some operations, known as pseudo-contractions, are in the middle ground between belief set change and belief base change. In the present work we have proposed a new pseudo-contraction operation, studied its properties and characterized it. We have also found connections between this operator and some other pseudo-contractions. / Revisão de Crenças aborda o problema de como alterar estados epistêmicos, normalmente representados na literatura como conjuntos de sentenças lógicas. Resultados teóricos sólidos foram consolidados com o paradigma AGM, que lida com teorias (conjuntos de sentenças logicamente fechados). Depois disso, a teoria foi estendida para bases de crenças, isto é, conjuntos arbitrários de sentenças. Apesar de todo esse arcabouço teórico, pesquisadores de IA enfrentam sérias dificuldades ao tentar implementar sistemas de revisão de crenças. Uma das maiores complicações é o fecho exigido pela teoria AGM, que não pode ser facilmente computado. Mesmo bases de crenças, que não exigem fechamento, parecem ser impróprias para fins práticos, pois suas alterações são geralmente muito rígidas (dependentes de sintaxe). Algumas operações, conhecidas como pseudo-contrações, estão no meio do caminho entre mudanças para conjuntos de crenças e mudanças para bases de crenças. Nesse trabalho, propomos uma nova operação de pseudo-contração, estudamos suas propriedades e a caracterizamos. Também encontramos conexões entre esse operador e algumas outras pseudo-contrações.

Belief Revision addresses the problem of how to change epistemic states, usually represented in the literature by sets of logical sentences. Solid theoretical results were consolidated with the AGM paradigm, which deals with theories (logically closed sets of sentences). After that, the theory was extended to belief bases, that is, arbitrary sets of sentences. Besides all this theoretical framework, AI researchers face serious difficulties when trying to implement belief revision systems. One of the major complications is the closure required by AGM theory, which cannot be easily computed. Even belief bases, which do not require closure, seem to be improper for practical purposes, since their changes are usually very rigid (syntax dependent). Some operations, known as pseudo-contractions, are in the middle ground between belief set change and belief base change. In the present work we have proposed a new pseudo-contraction operation, studied its properties and characterized it. We have also found connections between this operator and some other pseudo-contractions. / Revisão de Crenças aborda o problema de como alterar estados epistêmicos, normalmente representados na literatura como conjuntos de sentenças lógicas. Resultados teóricos sólidos foram consolidados com o paradigma AGM, que lida com teorias (conjuntos de sentenças logicamente fechados). Depois disso, a teoria foi estendida para bases de crenças, isto é, conjuntos arbitrários de sentenças. Apesar de todo esse arcabouço teórico, pesquisadores de IA enfrentam sérias dificuldades ao tentar implementar sistemas de revisão de crenças. Uma das maiores complicações é o fecho exigido pela teoria AGM, que não pode ser facilmente computado. Mesmo bases de crenças, que não exigem fechamento, parecem ser impróprias para fins práticos, pois suas alterações são geralmente muito rígidas (dependentes de sintaxe). Algumas operações, conhecidas como pseudo-contrações, estão no meio do caminho entre mudanças para conjuntos de crenças e mudanças para bases de crenças. Nesse trabalho, propomos uma nova operação de pseudo-contração, estudamos suas propriedades e a caracterizamos. Também encontramos conexões entre esse operador e algumas outras pseudo-contrações.

Verificação de modelos é uma das mais eficientes técnicas de verificação automática de sistemas. No entanto, apesar de poder lidar com verificações complexas, as ferramentas de verificação de modelos usualmente não fornecem informação alguma sobre como reparar inconsistências nestes modelos. Nesta dissertação, mostramos que abordagens desenvolvidas para a atualização de modelos CTL inconsistentes não são capazes de lidar com todos os tipos de alterações em modelos. Introduzimos então o conceito de revisão de modelos: uma abordagem baseada em revisão de crenças para o reparo de modelos inconsistentes em um contexto estático. Relacionamos nossa proposta com trabalhos clássicos em revisão de crenças. Definimos um operador de revisão de modelos e mostramos que este obedece postulados de racionalidade clássico de revisão de crenças. Propomos um algoritmo de revisão com base no algoritmo utilizado pela abordagem de atualização de modelos. Discutimos sobre problemas e limites do algoritmo proposto, e mostramos que essa estratégia de adaptação não é uma solução apropriada. / Model checking is one of the most robust techniques in automated system verification. But, although this technique can handle complex verifications, model checking tools usually do not give any information on how to repair inconsistent system models. In this dissertation, we show that approaches developed for CTL model update cannot deal with all kinds of model changes. We introduce the concept of CTL model revision: an approach based on belief revision to handle system inconsistency in a static context. We relate our proposal to classical works on belief revision. We define an operator for model revision and we show that it obeys the classical rationality postulates of belief revision. We propose an algorithm for model revision based on the algorithm used by the model update approach. We discuss problems and limitations of our proposed algorithm and show that this strategy of adaptation is not an appropriate solution.

Neste trabalho apresentamos uma implementação de revisão de crenças baseada em comparação de modelos (estados) em uma ferramenta de verificação automática de sistemas de estados finitos. Dada uma fórmula (na lógica CTL) inconsistente com o modelo do sistema, revisamos esse modelo de tal maneira que essa fórmula temporal se torne verdadeira. Como temos oito operadores temporais (AG, AF, AX, AU, EG, EF, EX e EU), foram criados algoritmos especícos para cada um deles. Como o modelo do sistema deriva do seu código na linguagem SMV, a sua revisão passa obrigatoriamente por mudanças na sua descrição. A nossa implementação contempla três tipos de mudanças: acréscimo de linhas, eliminação de linhas e mudança no estado inicial, sendo que as duas primeiras provocam modicações nas transições entre os estados que compõe o modelo. Alguns testes foram aplicados para comprovar a contribuição da revisão de crenças (revisão de modelos) como ferramenta de auxílio ao usuário durante o processo de modelagem de sistemas. / In this work we present an implementation of belief revision based on comparison of models (states) in a tool for automatic verication of nite state systems. Given a formula (in the language of CTL) inconsistent with the model of the system, we revise this model in such way that the temporal formula becomes valid. As we have eight temporal operators (AG, AF, AX, AU, EG, EF, EX and EU), specic algorithms for each one of them have been created. As the model of the system is related with its code in SMV language, its revision forces changes in its description. Our implementation contemplates three types of change: addition of lines, elimination of lines and change in the initial state, where the rst two cause modications in the transitions between the states of the model. Some tests were applied to prove the contribution of the belief revision (model revision) as aid-tool to the user during the process of systems modeling.

Uma importante etapa do desenvolvimento de software é o de levantamento e análise dos requisitos. Porém, durante esta etapa podem ocorrer inconsistências que prejudicarão o andamento do projeto. Além disso, após finalizada a especificação, o cliente pode querer acrescentar ou modificar as funcionalidades do sistema. Tudo isso requer que a especificação do software seja revista, mas isso é altamente custoso, tornando necessário um processo automatizado para simplificar tal revisão. Para lidar com este problema, uma das abordagens utilizadas tem sido o processo de Revisão de Crenças, juntamente com o processo de Verificação de Modelos. O objetivo deste trabalho é utilizar o processo de revisão de crenças e verificação de modelos para avaliar especificações de um projeto procurando inconsistências, utilizando o fragmento universal da Computation Tree Logic (CTL), conhecido como ACTL, e revisá-las gerando sugestões de mudanças na especificação. A nossa proposta é traduzir para lógica clássica tanto o modelo (especificação do software) quanto a propriedade a ser revisada, e então aplicar um resolvedor SAT para verificar a satisfazibilidade da fórmula gerada. A partir da resposta do resolvedor SAT, iremos gerar sugestões válidas de mudanças para a especificação, fazendo o processo de tradução reversa da lógica clássica para o modelo original. / The objective of this work is to join the proccess of belief revision and model checking to evaluate project specifications looking for inconsistences, using the universal fragment of Computation Tree Logic (CTL), known as ACTL, and revise them generating changes suggestions in the specification. Our approach will translate the model (software specification) and the property to be revised to classical logic. Then we will apply a SAT solver to verify the generated formulas satsifability. From the SAT solver answer, we will create changes valid suggestions to the specification making the translation back from classical logic to the original model. To generate the changes suggestions, we proposed a framework based on heuristics where different approaches and decisions can be implemented, aiming a better application for each project scope. We implemented a basic heuristic as an example and used it to test the implementation to analise the proposed algorithm

Uma importante etapa do desenvolvimento de software é o de levantamento e análise dos requisitos. Porém, durante esta etapa podem ocorrer inconsistências que prejudicarão o andamento do projeto. Além disso, após finalizada a especificação, o cliente pode querer acrescentar ou modificar as funcionalidades do sistema. Tudo isso requer que a especificação do software seja revista, mas isso é altamente custoso, tornando necessário um processo automatizado para simplificar tal revisão. Para lidar com este problema, uma das abordagens utilizadas tem sido o processo de Revisão de Crenças, juntamente com o processo de Verificação de Modelos. O objetivo deste trabalho é utilizar o processo de revisão de crenças e verificação de modelos para avaliar especificações de um projeto procurando inconsistências, utilizando o fragmento universal da Computation Tree Logic (CTL), conhecido como ACTL, e revisá-las gerando sugestões de mudanças na especificação. A nossa proposta é traduzir para lógica clássica tanto o modelo (especificação do software) quanto a propriedade a ser revisada, e então aplicar um resolvedor SAT para verificar a satisfazibilidade da fórmula gerada. A partir da resposta do resolvedor SAT, iremos gerar sugestões válidas de mudanças para a especificação, fazendo o processo de tradução reversa da lógica clássica para o modelo original. / The objective of this work is to join the proccess of belief revision and model checking to evaluate project specifications looking for inconsistences, using the universal fragment of Computation Tree Logic (CTL), known as ACTL, and revise them generating changes suggestions in the specification. Our approach will translate the model (software specification) and the property to be revised to classical logic. Then we will apply a SAT solver to verify the generated formulas satsifability. From the SAT solver answer, we will create changes valid suggestions to the specification making the translation back from classical logic to the original model. To generate the changes suggestions, we proposed a framework based on heuristics where different approaches and decisions can be implemented, aiming a better application for each project scope. We implemented a basic heuristic as an example and used it to test the implementation to analise the proposed algorithm

Neste trabalho apresentamos uma implementação de revisão de crenças baseada em comparação de modelos (estados) em uma ferramenta de verificação automática de sistemas de estados finitos. Dada uma fórmula (na lógica CTL) inconsistente com o modelo do sistema, revisamos esse modelo de tal maneira que essa fórmula temporal se torne verdadeira. Como temos oito operadores temporais (AG, AF, AX, AU, EG, EF, EX e EU), foram criados algoritmos especícos para cada um deles. Como o modelo do sistema deriva do seu código na linguagem SMV, a sua revisão passa obrigatoriamente por mudanças na sua descrição. A nossa implementação contempla três tipos de mudanças: acréscimo de linhas, eliminação de linhas e mudança no estado inicial, sendo que as duas primeiras provocam modicações nas transições entre os estados que compõe o modelo. Alguns testes foram aplicados para comprovar a contribuição da revisão de crenças (revisão de modelos) como ferramenta de auxílio ao usuário durante o processo de modelagem de sistemas. / In this work we present an implementation of belief revision based on comparison of models (states) in a tool for automatic verication of nite state systems. Given a formula (in the language of CTL) inconsistent with the model of the system, we revise this model in such way that the temporal formula becomes valid. As we have eight temporal operators (AG, AF, AX, AU, EG, EF, EX and EU), specic algorithms for each one of them have been created. As the model of the system is related with its code in SMV language, its revision forces changes in its description. Our implementation contemplates three types of change: addition of lines, elimination of lines and change in the initial state, where the rst two cause modications in the transitions between the states of the model. Some tests were applied to prove the contribution of the belief revision (model revision) as aid-tool to the user during the process of systems modeling.

Verificação de modelos é uma das mais eficientes técnicas de verificação automática de sistemas. No entanto, apesar de poder lidar com verificações complexas, as ferramentas de verificação de modelos usualmente não fornecem informação alguma sobre como reparar inconsistências nestes modelos. Nesta dissertação, mostramos que abordagens desenvolvidas para a atualização de modelos CTL inconsistentes não são capazes de lidar com todos os tipos de alterações em modelos. Introduzimos então o conceito de revisão de modelos: uma abordagem baseada em revisão de crenças para o reparo de modelos inconsistentes em um contexto estático. Relacionamos nossa proposta com trabalhos clássicos em revisão de crenças. Definimos um operador de revisão de modelos e mostramos que este obedece postulados de racionalidade clássico de revisão de crenças. Propomos um algoritmo de revisão com base no algoritmo utilizado pela abordagem de atualização de modelos. Discutimos sobre problemas e limites do algoritmo proposto, e mostramos que essa estratégia de adaptação não é uma solução apropriada. / Model checking is one of the most robust techniques in automated system verification. But, although this technique can handle complex verifications, model checking tools usually do not give any information on how to repair inconsistent system models. In this dissertation, we show that approaches developed for CTL model update cannot deal with all kinds of model changes. We introduce the concept of CTL model revision: an approach based on belief revision to handle system inconsistency in a static context. We relate our proposal to classical works on belief revision. We define an operator for model revision and we show that it obeys the classical rationality postulates of belief revision. We propose an algorithm for model revision based on the algorithm used by the model update approach. We discuss problems and limitations of our proposed algorithm and show that this strategy of adaptation is not an appropriate solution.

A área de revisão de crenças estuda a forma como agentes racionais operam sobre seus conhecimentos, permitindo que estes evoluam à vista de novas informações. Muitas das formas de manipulação do conhecimento hoje utilizadas foram desenvolvidas tendo como base o paradigma estabelecido por Alchourrón, Gärdenfors e Makinson em 1985, que evoluiu nas últimas décadas sob influência de diversas correntes de pensamento, dando origem a múltiplas abordagens para a estruturação de operadores sobre crenças. Esta dissertação limita-se à análise das duas principais construções de operadores sobre bases de crenças, bem como suas propriedades e relações. A partir desta análise, foi construído um framework computacional que permitiu a análise empírica do comportamento destas construções em diversos casos gerados, de modo a averiguar a eficiência real dos algoritmos envolvidos. Também são expostos detalhes do framework, construído de forma flexível para permitir sua reutilização em trabalhos futuros. / Belief revision studies the ways rational agents change their beliefs, allowing them to evolve when exposed to new information. Many of the belief change forms currently used were developed based on the paradigm established by Alchourrón, Gärdenfors and Makinson in 1985, which evolved over the last decades under the influence of several distinct fields, originating multiple approaches to implement operators on beliefs. This dissertation is limited to the analysis of the two main constructions of operators on belief bases, including their properties and relations. Based on this analysis, a computational framework was created to allow the empirical analysis of the behavior of these constructions on generated scenarios, in order to measure the real eficiency of the algorithms concerned. It also describes the framework, built aiming for exibility in order to allow it\'s usage in future works.

Orientador: Marcelo Esteban Coniglio / Tese (doutorado) - Universidade Estadual de Campinas, Instituto de Filosofia e Ciências Humanas / Made available in DSpace on 2018-08-25T18:45:14Z (GMT). No. of bitstreams: 1 Testa_RafaelRodrigues_D.pdf: 1707390 bytes, checksum: 77a5315394cfd4052cf1fe8733d0559c (MD5) Previous issue date: 2014 / Resumo: A Revisão de Crenças estuda como agentes racionais mudam suas crenças ao receberem novas informações. O sistema AGM, trabalho mais influente desta área apresentado por Alchourrón, Gärdenfos e Makinson, postula critérios de racionalidade para os diferentes tipos de mudança de crenças e oferece construções explícitas para tais - a equivalência entre os postulados e operações é chamado de teroema da representação. Trabalhos recentes mostram como o paradigma AGM pode ser compatível com diferentes lógicas não-clássicas, o que é chamado de AGM-compatibilidade - este é o caso da família de lógicas paraconsistentes que analisamos, as Lógicas da Inconsistência Formal (LFIs, da sigla em inglês). A despeito da AGM-compatibilidade, ao se partir de uma nova lógica sua racionalidade subjacente deve ser entendida e sua linguagem deve ser efetivamente usada. Propomos assim novas construções que de fato capturam a intuição presente na LFIs - é o que chamamos de sistema AGMo. Com isso, possibilitamos a estas lógicas uma nova interpretação, na esteira da epistemologia formal. Em uma abordagem alternativa, ao se partir da AGM-compatibilidade os resultados AGM podem ser diretamente aplicados às LFIs - o que chamamos de sistema AGMp. Em ambas abordagens, provamos os respectivos teoremas da representação sempre que necessário / Abstract: Belief Revision studies how rational agents change their beliefs when they receive new information. The AGM system, most influential work in this area of study investigated by Alchourrón, Gärdenfos and Makinson, postulates rationality criteria for different types of belief change and provides explicit constructions for them - the equivalence between the postulates and operations is called representation theorem. Recent studies show how the AGM paradigm can be compliant with different non-classical logics, which is called the AGM-compliance - this is the case of the paraconsistent logics family we analyze in this thesis, the Logics of Formal Inconsistency (LFIs). Despite the AGM-compliance, when a new logic is taken into account its underlying rationality must be understood and its language should be used. In that way new constructions are proposed, which actually captures the intuition of LFIs - what we call the AGMo system. Thus, we provide a new interpretation for these logics, more in line with formal epistemology. In an alternative approach, by considering the AGM-compliance, we show how the AGM results can be directly applied to LFIs -- resulting the AGMp system. In both approaches, we prove the corresponding representation theorems where needed / Doutorado / Filosofia / Doutor em Filosofia