In order to specify properties relating to probability, real time, and knowledge on multi-agent systems, a logic system PTCTLK is proposed. Model checking is an automatic technique for checking if a multi-agent system satisfies a PTCTLK formula. The state explosion problem is the key obstacle in checking the feasibility of the model. In this paper, a bounded model checking algorithm for PTCTLK is proposed. First the model checking of PTCTLK is reduced to the model checking of PBTLK, which does not contain real time operators. Second, the bounded semantics of PBTLK is defined and its correctness is proven. Third, the bounded model checking procedure of PBTLK is transformed into a linear equation. Finally, the paper discusses the law of increasing of probability measure, and some termination criterions are given. The case study shows that compared with the unbounded model checking, if the length of the witness is short, then the bounded model checking needs less space.