Common Knowledge in Well-structured Perfect Recall Systems

Abstract

We investigate a model checking problem for the logic of common knowledge and fixpoints µPLCn in well-structured multiagent systems with perfect recall. In this paper we show that a perfect recall synchronous environment over a well-structured environment forms a well-structured environment provided with a special PRS-order. This implies that the model checking problem for the disjunctive fragment of µPLCn is decidable.

Keywords

• логика общих знаний
• мультиагентные системы с абсолютной памятью
• хорошо структурированные системы
• проверка моделей