Bo Sun Conghua Zhou, Liu Zhifeng

*Artificial Intelligence and Computational Intelligence*

Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence) 6319

Springer

2010

Probabilistic temporal logics of knowledge have been used to specify multi-agent systems. In this paper, we introduce a probabilistic temporal logic of knowledge called PTLK for expressing time, knowledge, and probability in multi-agent systems. Then, in order to overcome the state explosion in model checking PTLK we propose an abstraction procedure for model checking PTLK. The rough idea of the abstraction approach is to partition the state space into several equivalence classes which consist of the set of abstract states. The probability distribution between abstract states is defined as an interval for computing the approximation of the concrete system. Finally, the model checking algorithm in PTLK is developed.

*keywords*
agent - model checking - abstraction - probabilistic logic - temporal logic - epistemic logic

journal or series

Lecture Notes in Computer Science

(LNCS)