Verification of Multi-agent Systems Via Bounded Model Checking

File Size Format
40254.pdf 151Kb Adobe PDF View
Title Verification of Multi-agent Systems Via Bounded Model Checking
Author Luo, Xiangyu; Su, Kaile; Sattar, Abdul; Reynolds, Mark
Publication Title AI 2006: Advances in Artificial Intelligence
Editor Abdul Sattar and Byeong-Ho Kang
Year Published 2006
Place of publication Berlin
Publisher Springer
Abstract 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 skilfully 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.
Peer Reviewed Yes
Published Yes
Publisher URI
Copyright Statement Copyright 2006 Springer : Reproduced in accordance with the copyright policy of the publisher : The original publication will be available at SpringerLink (use hypertext links)
ISBN 3-540-49787-0
Conference name 19th Australian Joint Conference on Artificial Intelligence
Location Hobart
Date From 2006-12-04
Date To 2006-12-08
Date Accessioned 2007-03-02
Language en_AU
Research Centre Institute for Integrated and Intelligent Systems
Faculty Faculty of Science, Environment, Engineering and Technology
Subject Other Artificial Intelligence
Publication Type Conference Publications (Full Written Paper - Refereed)
Publication Type Code e1

Show simple item record

Griffith University copyright notice