Abschlussarbeit

Beschreibung:

The need to represent and reason about time arises in many applications of AI, such as in multi-agent scenarios and reasoning about sensing actions. A rational agent often does not have a complete observation of the domain, but only a partial description of it. Explicitly representing that an agent is ignorant about certain pieces of information is important, as these information might impact the decisions an agent makes. Guerra et al. [1] have proposed to use a KMTS (Kripke Modal Transition System) as a model to explicitly represent ignorance of temporal information. As new pieces of information arrive, an agent needs to check if they are not conflicting with its current body of knowledge before incorporating the new information. When the new piece of information conflicts with the agent’s current body of knowledge, the agent should be capable of identifying which parts of
its body of knowledge are responsible for the clash and remove them. In short, maintenance of a body of knowledge involves two main problems: consistency checking, and pinpointing of knowledge conflicts. When temporal knowledge is represented as a model, such as a KMTS, consistency checking corresponds to the model checking problem: given a model M and a formula phi, does M satisfy phi?
Model Checking is a successful technique used on formal specification and verification of concurrent programs, and several approaches to extract and pinpoint knowledge conflicts based on model checking techniques were proposed in the literature. Most of the model checking techniques, however, do not capture precisely the interpretation given by Guerra et al. on KMTSs to explicitly represent ignorance awareness. Following this line, Ribeiro and Andrade [2] have proposed a novel model checking technique, based on game theory approaches, that captures precisely Guerra interpretation. For clash resolution, also using game-based model checking techniques, Guerra et al. have shown how to identify all the possible causes for clashes between a KMTS and a given formula of interest.

In this thesis, you will implement the model checking technique proposed by Ribeiro and Andrade and augment it with the capability of pinpointing knowledge conflicts presented by Guerra et al. An evaluation of the implementation will be carried out.

• [1] Paulo T. Guerra, Aline Andrade, and Renata Wassermann. “Toward the Revision of CTL Models through Kripke Modal Transition Systems”. In: Formal Methods: Foundations and Applications - 16th Brazilian Symposium, SBMF 2013, Proceedings. Vol. 8195, LNCS, Springer, 2013, pp. 115–130.
• [2] Jandson S. Ribeiro and Aline Andrade. “A 3-Valued Contraction Model Checking Game: Deciding on the World of Partial Information”. In: Formal Methods and Software Engineering - 17th International Conference on Formal Engineering Methods, ICFEM 2015, Proceedings. Vol. 9407, LNCS, Springer, 2015, pp. 84–99.