• 中国精品科技期刊
  • CCF推荐A类中文期刊
  • 计算领域高质量科技期刊T1类
Advanced Search
Wu Lijun, Su Kaile, Chen Qingliang, Yang Zhihua. Algorithm Research on “On the Fly” Model Checking Temporal Logics of Knowledge in Multi-Agent Systems[J]. Journal of Computer Research and Development, 2006, 43(8): 1417-1424.
Citation: Wu Lijun, Su Kaile, Chen Qingliang, Yang Zhihua. Algorithm Research on “On the Fly” Model Checking Temporal Logics of Knowledge in Multi-Agent Systems[J]. Journal of Computer Research and Development, 2006, 43(8): 1417-1424.

Algorithm Research on “On the Fly” Model Checking Temporal Logics of Knowledge in Multi-Agent Systems

More Information
  • Published Date: August 14, 2006
  • Temporal logics of knowledge have been widely used in the distributed systems community and in the expression for the specifications of protocols. The model checking for temporal logics of knowledge becomes a new and important research domain. So approaches to the “on the fly” model checking the temporal logics of knowledge are discussed. Based on the “on the fly” model checking approaches for temporal logics, and according to automata theory and the semantics of knowledge, the “on the fly” model checking approaches to the temporal logics of knowledge are presented. These approaches, making the model checking for the specifications with knowledge operators, need only to construct a small portion of state space of system before a counterexample is found, and so avoid memory-shortage and state-explosion and realize “on the fly” model checking for the temporal logic of knowledge. And the time complexity of the algorithm is polynomial. Finally, the application to the verification of the TMN cryptographic protocol is illustrated to show the effectiveness of the approach.
  • Related Articles

    [1]Bai Tian, Xiao Mingyu. Computational Complexity of Feedback Set and Subset Feedback Set Problems: A Survey[J]. Journal of Computer Research and Development, 2025, 62(1): 104-118. DOI: 10.7544/issn1000-1239.202330693
    [2]Jiang Luyu, Ouyang Dantong, Zhang Qi, Tai Ran, Zhang Liming. Incremental Information Interaction-Based Method for Enumerating MUSes[J]. Journal of Computer Research and Development. DOI: 10.7544/issn1000-1239.202440326
    [3]Ouyang Dantong, Jia Fengyu, Liu Siguang, Zhang Liming. An Algorithm Based on Extension Rule For Solving #SAT Using Complementary Degree[J]. Journal of Computer Research and Development, 2016, 53(7): 1596-1604. DOI: 10.7544/issn1000-1239.2016.20150032
    [4]Li Shaohua, Feng Qilong, Wang Jianxin, and Chen Jianer. Kernelization for Weighted 3-Set Packing Problem[J]. Journal of Computer Research and Development, 2012, 49(8): 17811-786.
    [5]Qiu Jiangtao, Tang Changjie, Zeng Tao, Liu Yintian. Strategy of Revising Rules for Association Text Classification[J]. Journal of Computer Research and Development, 2009, 46(4): 683-688.
    [6]Zhong Yong, Qin Xiaolin, and Bao Lei. An Association Rule Mining Algorithm of Multidimensional Sets[J]. Journal of Computer Research and Development, 2006, 43(12): 2117-2123.
    [7]Xiong Zhongmin, Hao Zhongxiao. An Approach to Termination Decision for a Rule Set Based on Activation Path and Conditional Formula[J]. Journal of Computer Research and Development, 2006, 43(5): 901-907.
    [8]Hao Zhongxiao, Xiong Zhongmin. An Efficient Algorithm for Computing an Irreducible Rule Set in Active Database[J]. Journal of Computer Research and Development, 2006, 43(2): 281-287.
    [9]Hao Zhongxiao, Ren Chao, Zhao Lingqiang. Termination Analysis of Active Rule Based on Dependency Set[J]. Journal of Computer Research and Development, 2005, 42(12): 2199-2205.
    [10]Tian Daxin, Liu Yanheng, Li Yongli, Tang Yi. A Fast Matching Algorithm and Conflict Detection for Packet Filter Rules[J]. Journal of Computer Research and Development, 2005, 42(7): 1128-1135.

Catalog

    Article views (779) PDF downloads (637) Cited by()

    /

    DownLoad:  Full-Size Img  PowerPoint
    Return
    Return