不确定型模糊Kripke结构的计算树逻辑模型检测

• 作者: 李永明 潘海玉 范艳焕
• 来源期刊: 电子学报
• 学科: 工学
• 关键词: 模型检测 计算树逻辑 模糊逻辑 Kripke结构 时态逻辑
• 年，卷（期）: 2018,（1）
• 所属期刊栏目: 学术论文
• 页码范围: 152-159
• 页数: 8页
• 分类号: TP301.2
• 字数: 10169字
• 语种: 中文
• DOI: 10.3969/j.issn.0372-2112.2018.01.021

摘要

本文研究了不确定型模糊Kripke结构的计算树逻辑的模型检测问题,并说明了该问题可以在对数多形式时间内解决.首先给出了不确定型模糊Kripke结构的定义,引入了模糊计算树逻辑的语法和语义.为了刻画存在量词(E)和任意量词(V)在不确定型模糊Kripke结构中的两种语义解释,在模糊计算树逻辑语法中引入了路径量词(E)sup,(E)inf和(V)sup,Vinf,分别用于替换存在量词(E)和任意量词(V).其次讨论了基于不确定型模糊Kripke结构的计算树逻辑模型检测算法,特别地对于模糊计算树逻辑公式(E)suppUq,(V)suppUq,(E)infpUq和(V)infpUq分别给出时间复杂度为对数多项式时间的改进算法.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李永明	陕西师范大学计算机科学学院	165	505	12.0	16.0
2	范艳焕	陕西师范大学计算机科学学院	3	8	2.0	2.0
6	潘海玉	陕西师范大学计算机科学学院	1	5	1.0	1.0