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

被引:28
作者
薛艳 [1 ]
雷红轩 [2 ]
李永明 [1 ]
机构
[1] 陕西师范大学计算机科学学院
[2] 内江师范学院数学与信息科学学院
关键词
可能的Kripke结构; 可能性测度; 可能性计算树逻辑; 一致性;
D O I
暂无
中图分类号
TP301.6 [算法理论];
学科分类号
080201 [机械制造及其自动化];
摘要
首先,提出了可能的Kripke结构的定义,建立了可能的Kripke结构的可能性测度空间,并分析了可能的Kripke结构的一系列性质,即任一路径转移的可能性可由其初始状态的可能性分布与各转移的可能性取下确界而得到;依据可能的Kripke结构所定义的可能性测度具有其合理性等等。其次,给出了可能性计算树逻辑(PoCTL)的概念,讨论了两个PoCTL状态公式以及PoCTL与经典计算树逻辑(CTL)公式的等价性。最后,证明了PoCTL公式有与CTL*公式中"一致性"相对应的公式。
引用
收藏
页码:70 / 75
页数:6
相关论文
共 4 条
[1]
A logic for reasoning about time and reliability.[J].Hans Hansson;Bengt Jonsson.Formal Aspects of Computing.1994, 5
[2]
AUTOMATIC VERIFICATION OF FINITE-STATE CONCURRENT SYSTEMS USING TEMPORAL LOGIC SPECIFICATIONS [J].
CLARKE, EM ;
EMERSON, EA ;
SISTLA, AP .
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1986, 8 (02) :244-263
[3]
模糊系统分析.[M].李永明著;.科学出版社.2005,
[4]
模糊测度与模糊积分理论.[M].哈明虎;吴从〓著;.科学出版社.1998,