Model checking, a formal and automatic verification method, has been widely used to check specifications expressed not only as qualitative properties (e.g safety and liveliness), but also as quantitative properties (e.g. degree of reliability and reachability). In this paper, we present a method for probabilistic model checking of multi-agent systems specified by a probabilistic-epistemic logic PCTLK. We define transformations from probabilistic interpreted systems into Discrete-time Markov chains (DTMC) and from PCTLK formulae to PCTL formulae so that we are able to convert the problem of model checking PCTLK to the one of PCTL. The algorithm is implemented in the probabilistic model checker PRISM. Some properties, including agents' probabilistic knowledge, are verified and simulations are shown.