Lógicas temporais são a base da área de verificação formal de sistemas. Em verificação formal, um sistema é descrito em uma linguagem formal e verificado frente um conjunto de propriedades desejadas, usualmente descritas por fórmulas de uma lógica modal. Apesar de técnicas de verificação formal poderem lidar com modelos complexos de sistema, ferramentas de verificação usualmente não auxiliam no processo de reparar uma especificação inconsistente. O objetivo intuitivo é remover tal inconsistência com mudanças mínimas na especificação original. Revisão de crenças trata do problema de como um agente racional deve adaptar suas crenças de modo a incorporar novas informações. Quando crenças e nova informação são inconsistentes, essa adaptação envolve desistência de crenças de modo que a consistência seja restaurada. A Teoria AGM de revisão de crenças propõe princípios básicos de racionalidade para esse processo, para que nessa adaptação de crenças o agente, por exemplo, não desista de crenças desnecessariamente. Trabalhos recentes em verificação formal desenvolvem abordagens que enriquecem métodos de verificação com princípios de mudanças de crenças, de modo a, por exemplo, modificar modelos de sistemas para que se tornem consistentes com uma dada propriedade temporal. Todavia, uma aplicação completa da teoria de revisão de crenças demanda a reformulação de diversos resultados clássicos para o formalismo de lógicas temporais. O problema ocorre porque lógicas temporais não satisfazem suposições clássicas, como o fato de serem lógicas compactas. Neste trabalho investigamos o uso de revisão de crenças sobre lógicas temporais, como objetivo criar fundamentações teóricas para a completa utilização desta teoria no reparo de especificações inconsistentes. Mostramos que o problema do reparo de especificação é dependente da perspectiva adotada pelo projetista sobre o significado desta especificação. Mostramos que fatores relativos a especificação de sistemas demandam duas abordagens distintas de revisão da especificação: uma abordagem baseada em conjuntos de fórmulas e outra baseada em modelos. A revisão de conjuntos de fórmulas temporais é uma abordagem semelhante as abordagens clássicas de revisão de crenças. Contudo, mostramos que no caso geral tal abordagem é incomputável para lógicas temporais. Propomos então restrições ao problema que possibilitam a formulação de operadores de revisão de crenças e mostramos que essas restrições ainda são aplicáveis a diversos problemas práticos de verificação formal. A abordagem de revisão de modelos é a adotada em diversos trabalhos recentes. Mostramos que operações desse tipo podem ser caracterizadas por postulados de racionalidade semelhantes aos propostos na Teoria AGM. Investigamos também revisão de modelos no contexto de especificações parciais, estabelecendo a caracterização de princípios de racionalidade para este cenário.

Temporal logics are the basis of the area of formal system verification. In formal verification, a system is described in a formal language and then checked against a set of desired properties, usually described in some temporal logic formalism. Although this technique can handle complex verifications, formal verification tools usually do not give any information on how to repair in- consistent system models. Once an inconsistency is detected, the intuitive goal is to remove this inconsistency through minimal changes in the original specification. Belief revision addresses the problem of how idealized agents should change their beliefs when receiving new information. When this information is inconsistent with the agent2019s beliefs, this change may involve withdrawal of some beliefs in order to restore consistency. The AGM theory of belief revision propose a minimality rationality principles that any rational agent should satisfies. Recent works in formal verification build approaches that improve formal verification methods with some principles of AGM or other related change theories. These approaches modify a model of a system, in order to make it consistent with some temporal formula. However, the full application of AGM theory demands a reformulation of several classical results for the temporal formalism. The AGM theory of belief revision has been successfully applied to families of logics satisfying certain assumptions, as being compact. For non-compact logics, which includes most of the temporal logics, there are still no general results that can be used. In this work we investigate the application of the AGM paradigm to temporal logics. The goal is to establish theoretical foundations for the full use of this theory in the repair of inconsistent specifications. We show that the problem of specification repair is dependent of the perspective adopted by the designer with respect to the specification. We show that the repair problem demands two distinct approaches: a revision approach based on sets of formulas and other based on model. The revision of sets of temporal formulas is an approach similar to the classic approaches in belief revision. We show, however, that such approach is incomputable to temporal logics in the general case. We then propose restrictions on the problem such that we could correctly formulate belief revision operators to temporal logic. We show although the restriction, our approach could still be applied to several problems in formal verification. The model-based approach is related to that used by most of the recent works in automa- ted model repair. We show that repair operations can be characterized by AGM-style rationality postulates. We also explore the model revision approach for partial specifications, giving also the characterizations properties in this context.