Model Checking Knowledge and Linear Time: PSPACE Cases

We present a general algorithm scheme for model checking logics of knowledge, common knowledge and linear time, based on simulations to a class of structures that capture the way that agents update their knowledge. We show that the scheme leads to PSPACE implementations of model checking the logic of knowledge and linear time in several special cases: perfect recall systems with a single agent or in which all communication is by synchronous broadcast, and systems in which knowledge is interpreted using either the agents’ current observation only or its current observation and clock value. In all these results, common knowledge operators may be included in the language. Matching lower bounds are provided, and it is shown that although the complexity bound matches the PSPACE complexity of the linear time temporal logic LTL, as a function of the model size the problems considered have a higher complexity than LTL.

• Type: Conference
• Year: 2007
• Where: LFCS
• Authors: Kai Engelhardt, Peter Gammie, Ron van der Meyden
• Keywords: Common Knowledge, LFCS 2007, Linear Time, Model Checking