Common Knowledge in Well-structured Perfect Recall Systems

We investigate a model checking problem for the logic of common knowledge and fixpoints $\mu$PLC$_n$ 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 $\mu$PLC$_n$ is decidable.