Title: The Complexity of Model Checking for Knowledge Update
Authors: Chitta Baral and Yan Zhang
Abstract
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.