文献类型：期刊文章

作　　者：范艳焕[1,2] 李永明[1] 潘海玉[1,3]

机构地区：[1]陕西师范大学计算机科学学院,陕西西安710062 [2]青海师范大学民师院数学系,青海西宁810008 [3]泰州学院计算机科学与技术学院,江苏泰州225300

出　　处：《电子学报》

基　　金：国家自然科学基金(No.11671244;No.61261047;No.61672023;No.61673352);教育部博士点基金(No.20130202110001);青海省自然科学基金(No.2014-ZJ-908);江苏高校"青蓝工程"

年　　份：2018

卷　　号：46

期　　号：1

起止页码：152-159

语　　种：中文

收录情况：BDHX、BDHX2017、CAS、CSA、CSA-PROQEUST、CSCD、CSCD2017_2018、EI、IC、JST、RCCSE、RSC、SCOPUS、ZGKJHX、核心刊

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

关 键 词：模型检测  计算树逻辑 模糊逻辑 KRIPKE结构 时态逻辑

分 类 号：TP301.2]