[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(
)
知识时态逻辑有界模型检测中的完备性
)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
- 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.
- 为解决限界模型检测的完备性问题, 研究了完全界的计算问题, 给出了完全界的上近似计算.首先, 在线性时态认知逻辑中引入过去时态算子, 得到新的时态认知逻辑LTLKP, 从而可以紧凑自然地描述系统的可靠性规范;其次, 依据图结构理论, 设计了一套深度优先算法计算出系统的最大可达深度和最长无循环路径的长度;最后, 以定理的形式给出了最大可达深度和最长无循环路径的长度与完全界的关系, 得出了完全界的一种上近似估算.所做工作有效地解决了限界模型检测中的完全界计算问题, 从而保证了限界模型检测的完备性.
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.