With the recent development of many model-checkers for the temporal logic of knowledge, abstraction techniques are necessary to increase the size of the systems that can be verified. In this paper, we introduce several abstraction techniques for interpreted systems and we prove several preservation results. These results consider the temporal logic of knowledge under Kleene's 3-valued interpretation along infinite and maximal finite paths.
"Proceedings of 5th Central and Eastern European Conference on Multi-Agent Systems (CEEMAS 2007)", Leipzig, 25-27 September 2007, Springer Verlag Lecture Notes in Computer Science volume 4696, pages 11-21, 2007.