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.

@article{conghuaZhifeng10,
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}
}
Tags:

Publication

— authors

Bo Sun Conghua Zhou, Liu Zhifeng

— status

published

— sort

article in journal

Venue

— journal

Lecture Notes in Computer Science

— volume

6319

— publication date

2010

URLs

original page  |  original PDF

Identifiers

— DOI

10.1007/978-3-642-16530-6_26

BibTeX

— BibTeX ID
conghuaZhifeng10
— BibTeX category
article

Partita IVA: 01131710376 - Copyright © 2008-2021 APICe@DISI Research Group - PRIVACY