|Table of Contents|

[1] Liu Zhifeng, Ge Yun, Zhang Dong, et al. Completeness of bounded model checking temporal logic of knowledge [J]. Journal of Southeast University (English Edition), 2010, 26 (3): 399-405. [doi:10.3969/j.issn.1003-7985.2010.03.006]
Copy

Completeness of bounded model checking temporal logic of knowledge()
Share：

Journal of Southeast University (English Edition)[ISSN:1003-7985/CN:32-1325/N]

Volumn:
26
Issue:
2010 3
Page:
399-405
Research Field:
Computer Science and Engineering
Publishing date:
2010-09-30

Info

Title:
Completeness of bounded model checking temporal logic of knowledge
Author(s):
Liu Zhifeng1;  2;  Ge Yun1;  Zhang Dong1;  Zhou Conghua2
1School of Electronic Science and Engineering, Nanjing University, Nanjing 210093, China
2School of Computer Science and Telecommunication Engineering, Jiangsu University, Zhenjiang 212013, China
Keywords:
bounded model checking;  temporal logics of knowledge;  multi-agent system
PACS:
TP311
DOI:
10.3969/j.issn.1003-7985.2010.03.006
Abstract:
In order to find the completeness threshold which offers a practical method of making bounded model checking complete, the over-approximation for the complete threshold is presented. First, a linear logic of knowledge is introduced into the past tense operator, and then a new temporal epistemic logic LTLKP is obtained, so that LTLKP can naturally and precisely describe the system’s reliability. Secondly, a set of prior algorithms are designed to calculate the maximal reachable depth and the length of the longest of loop free paths in the structure based on the graph structure theory. Finally, some theorems are proposed to show how to approximate the complete threshold with the diameter and recurrence diameter. The proposed work resolves the completeness threshold problem so that the completeness of bounded model checking can be guaranteed.

References:

[1] Clarke E M, Grumberg O, Peled D. Model checking[M]. Massachusetts: MIT Press, 2000.
[2] Nguyen V Y, Ruys T C. Incremental hashing for spin[C]//Lecture Notes in Computer Science. Berlin: Springer-Verlag, 2008, 5156: 232-249.
[3] Zaks A, Joshi R. Verfying multi-threaded C programs with SPIN[C]//Lecture Notes in Computer Science. Berlin: Springer-Verlag, 2008, 5156: 325-342.
[4] Vardi M Y. Branching vs. linear time: final showdown[C]//Proceedings of the Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin: Springer-Verlag, 2001: 1-22.
[5] McMillan K L. Symbolic model checking[M]. Boston, MA, USA: Kluwer Academic Publishers, 1993.
[6] Fagin R, Halpern J, Vardi M Y. A model-theoretic analysis of knowledge[J]. Journal of the ACM, 1991, 38(2): 382-428.
[7] Fagiu R, Halperu J Y, Moses Y, et al. Reasoning about knowledge[M]. Massachusetts: MIT Press, 1995.
[8] Jamroga W, Dix J. Model checking abilities of agents: a closer look[J]. Theory of Computing Systems, 2008, 42(3): 366-410.
[9] Penczek W, Lomuscio A. Verifying epistemic properties of multi-agent systems via bounded model checking[J]. Fundamenta Informaticae, 2003, 55(2):167-185.
[10] Luo Xiangyu, Su Kaile, Sattar A, et al. Bounded model checking knowledge and branching time in synchronous multi-agent systems[C]//Proc of the 4th Intl Joint Conf on Autonomous Agents and Multiagent Systems. New York: ACM Press, 2005: 1129-1130.
[11] Wozna B, Lomuscio A, Penczek W. Bounded model checking for knowledge and real time[C]//Proc of the 4th Intl Joint Conf on Autonomous Agents and Multiagent Systems. New York: ACM Press, 2005:165-172.
[12] Wozna B, Lomuscio A, Penczek W. Bounded model checking for deontic interpreted systems[C]//Proc of LCMAS’04. The Netherlands: Elsevier, 2004, 126: 93-114.
[13] Ben-Ari M, Manna Z, Pnueli A. The temporal logic of branching time[J]. Acta Information, 1983, 20: 207-226.
[14] Penczek W, Wozna B, Zbrzezny A. Bounded model checking for the universal fragment of CTL[J]. Fundamenta Informaticae, 2002, 51(1): 135-156.
[15] Wozna B. ACTL* properties and bounded model checking[J]. Fundamenta Informaticae, 2004, 63(1):65-87.
[16] Pnueli A. A temporal logic of concurrent programs[J].Theoretical Computer Science, 1983, 13(1): 45-60.
[17] Clarke E, Kroening D, Ouaknine J, et al. Completeness and complexity of bounded model checking[C]//Lecture Notes in Computer Science. Berlin: Springer-Verlag, 2004, 2937: 85-96.
[18] Benedetti M, Cimatti A. Bounded model checking for past LTL[C]//Lecture Notes in Computer Science. Berlin: Springer-Verlag, 2003, 2619: 18-33.
[19] Biere A, Cimatti A, Clarke E M, et al. Symbolic model checking without BDDs[C]//Lecture Notes in Computer Science. Berlin: Springer-Verlag, 1999, 1579:193-207.
[20] Hoek W V D, Wooldridge M. Tractable multiagent planning for epistemic goals[C]//Proc of the First International Conference on Autonomous Agents and Multi-Agent Systems. New York: ACM, 2002:1167-1174.

Memo

Memo:
Biographies: Liu Zhifeng(1981—), male, graduate; Zhou Conghua(corresponding author), male, doctor, associate professor, chzhou@ujs.edu.cn.
Foundation items: The National Natural Science Foundation of China(No.10974093), the Scientific Research Foundation for Senior Personnel of Jiangsu University(No.07JDG014), the Natural Science Foundation of Higher Education Institutions of Jiangsu Province(No.08KJD520015).
Citation: Liu Zhifeng, Ge Yun, Zhang Dong, et al. Completeness of bounded model checking temporal logic of knowledge[J].Journal of Southeast University(English Edition), 2010, 26(3):399-405.
Last Update: 2010-09-20