广义可能性计算树逻辑的两种范式

• 作者: 李永明 赵杰
• 来源期刊: 计算机科学与探索
• 学科: 工学
• 关键词: 广义可能性测度 计算树逻辑 范式 模型检测
• 年，卷（期）: 2016,（10）
• 所属期刊栏目: 理论与算法
• 页码范围: 1475-1481
• 页数: 7页
• 分类号: TP301.2
• 字数: 5923字
• 语种: 中文
• DOI: 10.3778/j.issn.1673-9418.1507053

摘要

计算树逻辑(computation tree logic,CTL)的范式在模型检测方法中具有重要意义,但基于广义可能性测度的计算树逻辑的范式尚未有系统研究.为了进一步完善广义可能性计算树(generalized possibilistic computation tree logic,GPoCTL)理论,在现有的广义可能性计算树逻辑理论的基础上,参考经典计算树逻辑的范式,给出了广义可能性计算树逻辑的两种不同的范式——正态范式(positive normal form,PNF)和存在范式(existential normal form,ENF),及其对应的语构和语义解释.最后利用归纳假设法证明了任意的广义可能性计算树逻辑公式都有与之等价的PNF公式和ENF公式.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李永明	陕西师范大学计算机科学学院	165	505	12.0	16.0
2	赵杰	陕西师范大学计算机科学学院	17	112	6.0	10.0