• 中国计算机学会会刊
  • 中国科技核心期刊
  • 中文核心期刊

J4 ›› 2011, Vol. 33 ›› Issue (9): 70-75.

• 论文 • 上一篇    下一篇

基于可能性测度的计算树逻辑

薛艳1,雷红轩2,李永明1   

  1. (1.陕西师范大学计算机科学学院,陕西 西安 710062;
    2.内江师范学院数学与信息科学学院,四川 内江 641112)
  • 收稿日期:2011-05-20 修回日期:2011-07-26 出版日期:2011-09-25 发布日期:2011-09-25
  • 作者简介:薛艳(1986),女,河南太康人,硕士生,研究方向为模型检测。雷红轩〖HT5"SS〗(1967),男,陕西洋县人,博士,副教授,研究方向为多值模型检测。李永明(1966),男,陕西大荔人,博士,教授,研究方向为计算智能、模糊系统分析、量子逻辑、量子计算、模型检测。

Computation Tree Logic Based on Possibility Measure

XUE Yan1,LEI Hongxuan2,LI Yongming1   

  1. (1.School of Computer Science,Shaanxi Normal University,Xi’an 710062;
    2.School of Mathematics and Information Science,Neijiang Normal University,Neijiang 641112,China)
  • Received:2011-05-20 Revised:2011-07-26 Online:2011-09-25 Published:2011-09-25

摘要:

首先,提出了可能的Kripke结构的定义,建立了可能的Kripke结构的可能性测度空间,并分析了可能的Kripke结构的一系列性质,即任一路径转移的可能性可由其初始状态的可能性分布与各转移的可能性取下确界而得到;依据可能的Kripke结构所定义的可能性测度具有其合理性等等。其次,给出了可能性计算树逻辑(PoCTL)的概念,讨论了两个PoCTL状态公式以及PoCTL与经典计算树逻辑(CTL)公式的等价性。最后,证明了PoCTL公式有与CTL*公式中“一致性”相对应的公式。

关键词: 可能的Kripke结构, 可能性测度, 可能性计算树逻辑, 一致性

Abstract:

Firstly, the definition of possibilistic Kripke structure is presented, and the possibility measure space based on it is established. The properties of possibilistic Kripke structure are discussesd, such as the possibility of each path is the infimum of the initial distribution and all of the transisiton possibilities, and the possibility measure which is defined in accordance with the possibilistic Kripke structure is reasonable, etc. Secondly, the possibility computation tree logic (PoCTL) is defined, the equivalence between two PoCTL formulae is studied, and the problems whether some PoCTL formulae are equivalent to some CTL formulae are analyzed. Finally, the persistence property corresponding to PoCTL in CTL*are proved.

Key words: possibilistic Kripke structure;possibility measure;possibility computation tree logic;persistence property