We consider the problem of how an agent's knowledge can be updated. We propose a formal method of knowledge update on the basis of the semantics of modal logic S5. In our method, an update is specified according to the minimal change on both the agent's actual world and knowledge. We discuss general minimal change properties of knowledge update and show that our knowledge update operator satisfies all Katsuno and Mendelzon's update postulates. We characterize several specific forms of knowledge update which have important applications in reasoning about change of agents' knowledge. We also examine the persistence property of knowledge and ignorance associated with knowledge update. We then investigate the computational complexity of model checking for knowledge update. We first show that in general the model checking for knowledge update is P 2 -complete, which places the problem at the same layer in the polynomial hierarchy of the traditional model based belief up...