Verification of Multi-agent Systems Via Bounded Model Checking


Xiangyu Luo, Kaile Su, Abdul Sattar, Mark Reynolds

We present a bounded model checking (BMC) approach to the verification of temporal epistemic properties of multi-agent systems. We extend the temporal logic CTL * by incorporating epistemic modalities and obtain a temporal epistemic logic that we call CTL * K. CTL * K logic is interpreted under the semantics of synchronous interpreted systems. Though CTL * K is of great expressive power in both temporal and epistemic dimensions, we show that BMC method is still applicable for the universal fragment of CTL * K. We present in some detail a BMC algorithm and prove its correctness. In our approach, agents’ knowledge interpreted in synchronous semantics can be skillfully attained by the state position function, which avoids extending the encoding of the states and the transition relations of the plain temporal epistemic model for time domain.

(keywords) bounded model checking - multi-agent systems - temporal epistemic logic - bounded semantics

AI 2006: Advances in Artificial Intelligence 19th Australian Joint Conference on Artificial Intelligence, Hobart, Australia, December 4-8, 2006. Proceedings, Lecture Notes in Computer Science 4304,  2006, Springer.

@article{boundedVerification06,
Author = {Luo, Xiangyu and Su, Kaile and Sattar, Abdul and Reynolds, Mark},
Journal = {Lecture Notes in Computer Science},
Title = {Verification of Multi-agent Systems Via Bounded Model Checking},
Volume = {4304},
Year = {2006},
Publisher = {Springer},
DOI = {10.1007/11941439_11}
}
Tags:

Publication

— authors

Xiangyu Luo, Kaile Su, Abdul Sattar, Mark Reynolds

— status

published

— sort

paper in proceedings

Venue

— volume

AI 2006: Advances in Artificial Intelligence 19th Australian Joint Conference on Artificial Intelligence, Hobart, Australia, December 4-8, 2006. Proceedings

— series

Lecture Notes in Computer Science

— volume

4304

— publication date

2006

URLs

original page  |  original PDF

Identifiers

— DOI

10.1007/11941439_11

BibTeX

— BibTeX ID
boundedVerification06
— BibTeX category
article

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