Title: The Complexity of Model Checking for Knowledge Update

Authors: Chitta Baral and Yan Zhang


The authors have recently proposed a formal theory of knowledge update based on the semantics of modal logic S5 \cite{bz:01}. In that system, an agent's knowledge set is represented as a S5 formula and update on agent's knowledge is implemented by updating the corresponding Kripke models of the agent's knowledge set. In this paper, we further investigate the computational complexity of model checking for knowledge update. We first show that in general the model checking for knowledge update is $\Sigma_{3}^{P}$-complete, which places the problem at one layer higher in the polynomial hierarchy than the traditional model based belief update (e.g. PMA). We then identify a subclass of knowledge update problems that has polynomial time complexity for model checking. We point out that some important knowledge update problems belong to this subclass. We also address other subclasses of knowledge update problems for which the complexity of model checking ranges from NP-complete to $\Sigma_{2}^{P}$-complete.