Complexity Study of Knowledge and Public Observation

Abstract

Automated planning has been a steady branch of research in the field of Artificial Intelligence. A very interesting branch of such planning studies is epistemic planning. Epistemic plans are such plans where the attained goal revolves around knowledge of some intelligent agents. One of the more popular modeling techniques and underlying language to handle knowledge of intelligent agents is provided by dynamic epistemic logic (DEL). It uses Kripke models that have possible states of truth and relations to model knowledge. It also uses a similar technique to model actions or events that update the knowledge state. Since DEL deals with how actions updating knowledge, it provides a natural way to deal with epistemic planning. Besides DEL, there are several other logical frameworks as well dealing with change in knowledge. One of them is epistemic temporal logic LTL𝑘 . Deciding plan-existence problem using such logical frameworks are quite complicated and lie in the higher complexity classes. Epistemic planning has been proven to be undecidable. This is because in order to find a finite sequence of actions from a finite set, the updated knowledge models become arbitrarily large. The main motivation behind this thesis is this: Coming up with a decidable and much easier fragment of epistemic planning. In order to do that, we have taken the help of the modeling techniques and language of the logical framework called public observation logic (POL). POL deals with how public observations change knowledge of intelligent agents. This framework uses a similar modelling technique as DEL that uses Kripke models. However, in POL, each possible state of the model has a regular expression assigned to it. This expression expresses the set of expected observations in that particular possible state. The formulas also use operators with regular expressions to denote change in knowledge after some public observation. This thesis majorly deals with two problems: The first problem is the model-checking problem of POL. Here this thesis investigates the decidability of the problem. Moreover it also gives a tight complexity result. In addition to that, it also deals with fragments whose model-checking lie in much easier complexity classes. This problem finds application in epistemic planning. Considering the atomic observations as actions, using the Kleene star operator in regular expressions, one can decide whether there is a finite sequence of actions or a plan to achieve some change in knowledge.