Revision of temporal beliefs

Author(s)

Paulo de Tarso Guerra Oliveira

• Document type: Doctoral Thesis
• Press: São Paulo.
• Institution: Universidade de São Paulo (USP). Instituto de Matemática e Estatística (IME/SBI)
• Defense date: 2016-05-06
• Advisor: Renata Wassermann

Abstract

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 agent\2019s 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. (AU)

• FAPESP's process: 10/15392-3 - Revision of CTL Models
• Grantee: Paulo de Tarso Guerra Oliveira
• Support Opportunities: Scholarships in Brazil - Doctorate