Revisiting satisfiability and model-checking for CTLK with synchrony and perfect recall
We show that CTL with knowledge modalities but without common knowledge has an undecidable satisfiability problem in the synchronous perfect recall semantics. We also present an adaptation of the classical model-checking algorithm for CTL that handles knowledge operators.
Proceedings of the 9th International Workshop on Computational Logic in Multi-Agent Systems (CLIMA 2008), Dresden, Germany, 29th-30th September 2008, Lecture Notes in Artificial Intelligence vol. 5405, pages 117-131, 2008.