Sciweavers

Share
LFCS
2007
Springer

Model Checking Knowledge and Linear Time: PSPACE Cases

12 years 7 months ago
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.
Kai Engelhardt, Peter Gammie, Ron van der Meyden
Added 08 Jun 2010
Updated 08 Jun 2010
Type Conference
Year 2007
Where LFCS
Authors Kai Engelhardt, Peter Gammie, Ron van der Meyden
Comments (0)
books