Common Knowledge and Update in Finite Environments

AbstractLogics of knowledge have been shown to provide a useful approach to the high level specification and analysis of distributed systems. It has been proposed that such systems can be developed using knowledge- based protocols, in which agents' actions have preconditions that test their state of knowledge. Both computer-assisted analysis of the knowledge properties of systems and automated compilation of knowledge-based protocols require the development of algorithms for the computation of states of knowledge. This paper studies one of the computational problems of interest, the model checking problem for knowledge formulae in the S5nKripke structures generated by finite state environments in which states determine an observation for each agent. Agents are assumed to have perfect recall and may operate synchronously or asynchronously. It is shown that, in this setting, model checking of common knowledge formulae is intractable, but efficient incremental algorithms are developed for formulae containing only knowledge operators. Connections to knowledge updates and compilation of knowledge-based protocols are discussed