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...

• Type: Conference
• Year: 2005
• Where: ATAL
• Authors: Xiangyu Luo, Kaile Su, Abdul Sattar, Qingliang Chen, Guanfeng Lv
• Keywords: ATAL 2005, Epistemic, Synchronous Interpreted System, Temporal Epistemic Logic