@inproceedings{c9f78cce819a4c47a72fc5550c4093d8,
title = "The Complexity of Model Checking for Knowledge Update",
abstract = "The authors have recently proposed a formal theory of knowledge update based on the semantics of modal logic S5 (Barai \& Zhang 2001). 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 Σ2P is Incomplete, 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 Σ2P complete.",
author = "Chitta Baral and Yan Zhang",
note = "Publisher Copyright: {\textcopyright} Proceedings of the International Conference on Knowledge Representation and Reasoning.; 8th International Conference on Principles of Knowledge Representation and Reasoning, KR 2002 ; Conference date: 22-04-2002 Through 25-04-2002",
year = "2002",
language = "English (US)",
series = "Proceedings of the International Conference on Knowledge Representation and Reasoning",
publisher = "Association for the Advancement of Artificial Intelligence",
pages = "82--93",
editor = "Dieter Fensel and Fausto Giunchiglia and Deborah McGuinness and Mary-Anne Williams",
booktitle = "Proceedings of the 8th International Conference on Principles of Knowledge Representation and Reasoning, KR 2002",
}