电子学报2018，Vol.46Issue(1)：152-159,8.DOI:10.3969/j.issn.0372-2112.2018.01.021
不确定型模糊Kripke结构的计算树逻辑模型检测
Computation Tree Logic Model.Checking for Nondeterminisitc Fuzzy Kripke Structure
摘要
Abstract
This paper studys model-checking problem for FCTL (fuzzy computation tree logic) over nondeterministic fuzzy system and shows that it can be solved in linear-logarithmic running time in the size of the system.Firstly,we introduce NFKS (nondeterministic fuzzy kripke structure) which is adapted to model nondeterministic fuzzy system.The syntax and semantics of fuzzy computation tree logic over NFKS are presented.For describing two kinds of semantic explanation,we use path quantifiers (E) sup,(E) inf and (V) sup,(V)inf as substitutes for an existential path quantifier (E) and a universal path quantifier (V_ in the syntax of the CTL.Then,we study the model checking algorithm for fuzzy computation tree logic over NFKS.Furthermore,the improvement algorithms for FCTL formuleas (E)suppUq,(V) suppUq,(E)infpUq and (V)infpUq are given,whose time complexities are linear-logarithmic running time in the size of the system.关键词
模型检测/计算树逻辑/模糊逻辑/Kripke结构/时态逻辑Key words
model checking/computation tree logic/fuzzy logic/Kripke structure/temporal logic分类
信息技术与安全科学引用本文复制引用
范艳焕,李永明,潘海玉..不确定型模糊Kripke结构的计算树逻辑模型检测[J].电子学报,2018,46(1):152-159,8.基金项目
国家自然科学基金(No.11671244,No.61261047,No.61672023,No.61673352) （No.11671244,No.61261047,No.61672023,No.61673352）
教育部博士点基金(No.20130202110001) （No.20130202110001）
青海省自然科学基金(No.2014-ZJ-908) （No.2014-ZJ-908）
江苏高校“青蓝工程” （）
