Sciweavers

ATAL
2005
Springer

Bounded model checking knowledge and branching time in synchronous multi-agent systems

13 years 9 months ago
Bounded model checking knowledge and branching time in synchronous multi-agent systems
We present an approach to the verification of temporal epistemic properties in synchronous multi-agent systems (MAS) via bounded model checking (BMC). Based on the semantics of synchronous interpreted system, we extend the temporal logic CTL∗ by incorporating epistemic modalities and obtain the so-called temporal epistemic logic CTL∗ K. 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 by using the semantics of synchronous interpreted system. 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 relation of the plain temporal epistemic model for time domain. Categories and Subject Descriptors I.2.11 [Artificial Intelligence]: DAI-Multiagent systems General Terms Theory, Ve...
Xiangyu Luo, Kaile Su, Abdul Sattar, Qingliang Che
Added 26 Jun 2010
Updated 26 Jun 2010
Type Conference
Year 2005
Where ATAL
Authors Xiangyu Luo, Kaile Su, Abdul Sattar, Qingliang Chen, Guanfeng Lv
Comments (0)