首页    期刊浏览 2024年07月07日 星期日
登录注册

文章基本信息

  • 标题:THREE-VALUED ABSTRACTION IN MODEL CKECKING PROBABIBLISTIC REAL-TIME TEMPORAL LOGIC OF KNOWLEDGE
  • 本地全文:下载
  • 作者:ZHIFENG LIU ; BO SUN ; CONGHUA ZHOU
  • 期刊名称:Journal of Theoretical and Applied Information Technology
  • 印刷版ISSN:1992-8645
  • 电子版ISSN:1817-3195
  • 出版年度:2013
  • 卷号:48
  • 期号:3
  • 出版社:Journal of Theoretical and Applied
  • 摘要:

    Model checking in probabilistic real-time temporal logic of knowledge PTACTLK confronts the same challenge as in traditional model checking, that is the state space explosion problem. Abstraction is one of the most effective methods to alleviate the state space explosion problem, under the traditional framework of two-valued abstraction, the abstract model obtained using abstraction techniques is only the upper approximation of the original model. In this paper, we introduce three-valued abstraction into model checking probabilistic real-time temporal logic of knowledge, define the abstract model of a probabilistic real time interpreted system and present the three-valued semantics of PTACTLK on the abstract model. We prove that the abstract model obtained using the abstraction techniques is not only the upper approximation of the original model but also its lower approximation. At last, a simple communication protocol is adopted to illustrate the effectiveness of our abstraction techniques.

  • 关键词:Model Checking (MC); Probabilistic Real-time Temporal Logic of Knowledge (PRTLK); PTACTLK; State Space Explosion(SSE); Three-valued Abstraction(TA)
国家哲学社会科学文献中心版权所有