Parallel and complete model checking with linear complexity

被引：0
作者：
Wu, Xiaojuan [1 ]
Wu, Lijun [1 ]
Huang, Huijia [1 ]
Xue, Lei [1 ]
机构：
[1] School of Computer Science and Engineering, University of Electronic Science and Technology of China
来源：
Journal of Information and Computational Science | 2013年 / 10卷 / 05期
关键词：
Complete; Dfs; Linear complexity; Model checking; Parallel;
D O I：
10.12733/jics20101591
中图分类号：
学科分类号：
摘要：
In this paper, we present Parallel and Complete model checking algorithm. This algorithm can parallel find out all counterexamples of small system with linear complexity only by main memory. If the checked system with a large scale, the algorithm employs disks to store the states and searches out all the counterexamples whose I/O complexity is linear at any situation. With parallel technology, the searching procedure is accelerated by multiply. At the same time, we employ hash function to speed up the comparison. Our algorithm parallel starts from accepting states of system to find out accepting cycles. If system does not exist any accepting cycles, our algorithm would be terminated, because it means there are no counterexamples in system. It can save a lot of time. In the complexity analysis part, we compare our algorithm to another parallel algorithms, it shows the outperforms of our algorithm. © 2013 Binary Information Press.
引用
收藏
页码：1519 / 1529
页数：10
相关论文
共 16 条
  • [1] Clarke E.M., Emerson E.A., Synthesis of synchronization skeletons for branching time temporal logic, Logic of ProgramsWorkshop, Springer-Verlag Lecture Notes in Computer Science, 131, pp. 52-71, (1981)
  • [2] Korf R.E., Schultze P., Large-scale parallel breadth-first search, AAAI 2005, pp. 1380-1385
  • [3] Nichols B., Butler D., J. Farrell, Pthreads Programming
  • [4] Jabbar S., Edelkamp S., Parallel external directed model checking with linear I/O, VMCAI, Lecture Notes in Computer Science, 3855, pp. 237-251, (2006)
  • [5] Jabbar S., Edelkamp S., I/O efficient directed model checking, VMCAI, 3385, pp. 313-329, (2005)
  • [6] Nageshwara Rao V., Kumar V., Parallel depth-first search, Part I: Implementation, International Journal of Parallel Programming, 16, 6, pp. 479-499, (1987)
  • [7] Nageshwara Rao V., Kumar V., Parallel depth-first search, Part II: Analysis, International Journal of Parallel Programming, 16, 6, pp. 501-519, (1987)
  • [8] Heyman T., Geist D., Grumberg O., Schuster A., A scalable parallel algorithm for reachability analysis of very large circuits, Formal Methods in Systems Design, 21, pp. 317-338, (2002)
  • [9] Kumar V., Ramesh K., Rao V.N., Parallel best-first search or state-space graphs: A summary of results, (1988)
  • [10] Zhou R., Hasen E., Parallel structured duplicate detection, AAAI 2007, pp. 1217-1223
12