Abstraction for Model Checking the Probabilistic Temporal Logic of Knowledge

   page       BibTeX_logo.png   
Bo Sun Conghua Zhou, Liu Zhifeng
Artificial Intelligence and Computational Intelligence
Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence) 6319

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.

keywordsagent - model checking - abstraction - probabilistic logic - temporal logic - epistemic logic
journal or series
book Lecture Notes in Computer Science (LNCS)