The same challengs facing model checkings in probabilistic real-time temporal logic of knowledge PTACTLK is the same as traditional model one.That is the state space explosion problem.Abstraction is one of the most effective methods to alleviate the state space explosion problem.In order to alleviate the problem of the state space explosion in model checking probabilistic real-time temporal logic of knowledge

an abstraction technique is presented.For the real time part of PTACTLK

that is PTACTL

we adopt the abstract discrete clock valuations

and the infinite state space of a probabilistic real time was interpreted into a finite form.For the epistemic operator K in PTACTLK

the definition of epistemic equivalent to an agent between abstract states is given.We define the abstract model of the interpreted system in a probabilistic real time and present the semantics of PTACTLK on the abstract model.We prove that the abstract model obtained by using the abstraction techniques is the upper approximation of the original model.At last

a simple communication protocol is adopted to illustrate the effectiveness of our abstraction techniques.