логика общих знаний, мультиагентные системы с абсолютной памятью, хорошо структурированные системы, проверка моделей, Information technology, T58.5-58.64

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.