APICe » Publications » ConghuaZhifeng10

Abstraction for Model Checking the Probabilistic Temporal Logic of Knowledge

Bo Sun Conghua Zhou, Liu Zhifeng
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
Lecture Notes in Computer Science 6319, 2010, Springer
 Publisher = {Springer},
 Journal = {Lecture Notes in Computer Science},
 Author = {Conghua Zhou, Bo Sun and Zhifeng, Liu},
 Title = {Abstraction for Model Checking the Probabilistic Temporal Logic of Knowledge},
 Year = {2010},
 Volume = {6319},
 DOI = {10.1007/978-3-642-16530-6_26}