积分商城

最新搜索： 电源 ide手册 传感器 拼音输入 STM32CubeMX STM32入门教程
您现在的位置是：首页 > 技术资料 > 不确定型模糊Kripke结构的计算树逻辑模型检测
推荐星级：
  • 1
  • 2
  • 3
  • 4
  • 5

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

更新时间：2019-12-24 04:23:28 大小：1M 上传用户：守着阳光1985查看TA发布的资源 标签：计算树逻辑模型 下载积分：1分 评价赚积分 （如何评价?） 打赏 收藏 评论(0) 举报

资料介绍

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


部分文件列表

文件名 大小
不确定型模糊Kripke结构的计算树逻辑模型检测.pdf 1M

【关注B站账户领20积分】

部分页面预览

（完整内容请下载后查看）
1
Vol． 46 No． 1  
Jan． 2018  
第
期
电
子
学
报
2018  
1
ACTA ELECTRONICA SINICA  
年
月
Kripke  
不确定型模糊  
结构的计算  
树逻辑模型检测  
1，2  
1
1，3  
， ，  
范艳焕 李永明 潘海玉  
( 1．  
，
陕西师范大学计算机科学学院 陕西西安  
710062; 2．  
，
青海师范大学民师院数学系  
810008; 3．  
， 225300)  
泰州学院计算机科学与技术学院 江苏泰州  
青海西宁  
:
Kripke  
，
结构的计算树逻辑的模型检测问题 并说明了该问题可以在对数多  
摘
要
本文研究了不确定型模糊  
．
形式时间内解决 首先给出了不确定型模糊  
Kripke  
， ．  
结构的定义 引入了模糊计算树逻辑的语法和语义 为了刻画存在  
Kripke  
，
结构中的两种语义解释 在模糊计算树逻辑语法中引入了路径量词  
量词和任意量词在不确定型模糊  
，
，
，
．
Kripke  
sup inf 和sup inf 分别用于替换存在量词和任意量词其次讨论了基于不确定型模糊  
结构的计算树  
pUq  
和inf  
分别给出时间复杂度为对  
，
逻辑模型检测算法 特别地对于模糊计算树逻辑公式sup  
pUq，  
sup  
pUq， pUq  
inf  
．
数多项式时间的改进算法  
:
;
;
; Kripke  
;
关键词  
中图分类号  
URL: http: / /www． ejournal． org． cn  
模型检测 计算树逻辑 模糊逻辑  
结构 时态逻辑  
0372-2112 ( 2018) 01-0152-08  
DOI: 10． 3969 /j． issn． 0372-2112． 2018． 01． 021  
:
TP301. 2  
:
A
:
文章编号  
文献标识码  
电子学报  
Computation Tree Logic Model Checking for Nondeterminisitc  
Fuzzy Kripke Structure  
1，2  
1
1，3  
FAN Yan-huan ，LI Yong-ming ，PAN Hai-yu  
( 1． College of Computer Science，Shaanxi Normal University，Xi’an，Shaanxi 710062，China;  
2． Department of Mathematics in National Normal College，Qinghai Normal University，Xining，Qinghai 810008，China;  
3． College of Computer Science and Technology，Taizhou University，Taizhou，Jiangsu 225300，China)  
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 intro-  
duce 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  
，
sup inf  
and  
，
sup inf  
as substitutes for an existential path quantifier  
and a universal path  
quantifier  
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  
pUq， pUq， pUq and  
sup inf  
pUq are given，  
inf  
sup  
whose time complexities are linear-logarithmic running time in the size of the system．  
Key words: model checking; computation tree logic; fuzzy logic; Kripke structure; temporal logic  
False  
．
并给出反例 其中系统模型可以由  
Kripke  
结构或  
1
引言  
．
迁移系统刻画 模型检测已广泛应用于计算机软硬件  
［1，2］  
( model checking)  
:
的基本思想是 给定  
模型检测  
、 、  
系统 集成电路 通信协议等方面的分析验证中  
．
［3，4］  
，
系统模型和刻画系统性质的时序逻辑  
验证系统模  
，
经典的模型检测强调的是系统行为的绝对正确  
． ，  
型是否满足该公式 如果满足 则输出  
True;  
否则输出  
．
回答的是系统是否满足所需的性质 由于定量系统的  
: 2017-05-19;  
: 2017-08-14; :  
责任编辑 孙瑶  
收稿日期  
修回日期  
:
基金项目 国家自然科学基金  
( No． 11671244，No． 61261047，No． 61672023，No． 61673352) ;  
( No． 20130202110001) ;  
青海省自然  
教育部博士点基金  
( No． 2014-ZJ-908) ;  
“ ”  
江苏高校 青蓝工程  
科学基金  
153  
1
: Kripke  
范艳焕 不确定型模糊 结构的计算树逻辑模型检测  
第
期
，
存在 定量模型检测是利用模型检测的方法对定量系  
， t- ［0，1］ ，  
词的推广 其中 模是 上的单调递增 满足交换  
，
统进行自动的形式验证 定量分析其满足用户需求的  
， ， 1 ．  
律 结合律 且以 为单位元的二元运算 给定有限序列  
x ，x ，…，x ［0，1］， x x ．  
x
x …  
表示为     
1
． ，  
程度 最近十几年里 定量模型检测受到了很多学者的  
∈
0 i  
≤ ≤  
1
2
n
n
i
2
n
［1］  
［5 ～ 7］  
［14］  
，
，
，
关注 比如概率模型检测  
多值模型检测  
广义可  
其中概率模  
型检测针对的是随机系统 基本的随机系统模型是马  
( markov chain) ． ( markov  
Zadeh  
、Product  
逻辑 逻  
几类常见的模糊逻辑  
为
［8 ～ 11］  
［12，13］  
，
．
能性模型检测  
和模糊模型检测  
、Lukasiewicz Gdel  
逻辑和  
．
逻辑  
辑
，
3
Kripke  
不确定型模糊  
结构和模糊计算树  
尔可夫链  
马尔可夫决策过程  
逻辑  
decision process)  
，
是带有不确定性选择的马尔可夫链 其  
3． 1  
Kripke  
不确定型模糊  
结构  
．
概率空间与其不确定性选择有关  
广义可能性模型检测是由李永明  
们将模糊理论中的可能性测度与模型检测技术相结  
Kripke  
［14］  
［10，11］  
Kripke  
( S，AP，，L) ，  
δ 其  
模糊  
结构 是一个四元组  
，
等提出 他  
S
，: S  
是可数非空状态集合 δ  
F( X)  
是一个模糊状  
→
中
，AP  
，L: S  
F( AP)  
是模糊  
态转换函数  
是原子命题集  
→
，
．
合 其基本的系统模型是广义可能性  
结构 潘海  
．
标签函数  
FCTL  
玉等研究了基于任意模糊逻辑代数结构的  
模型  
［14］  
［15］  
1
Kripke  
( NFKS)  
是一个  
定义  
不确定型模糊  
结构  
CTL  
，
检测 和基于任意有限格的  
的模型检测问题  
M = ( S，Act，，AP，L) ，  
δ 其中  
:
五元组  
Kripke  
．
结构 这两者的模型  
其基本的系统模型是模糊  
．
结构特点是当前状态对应于一个模糊状态集 然而在  
( 1) S  
;
是一个可数非空状态集合  
( 2) Act  
;
是动作集合  
，
实际系统建模时存在这样的系统 在某一状态上后继  
( 3) : S × Act F( X)  
δ
→
，( s，a) ( t)  
是模糊转移函数 δ  
．
状态的选择是基于不确定的模糊选择 因此这样的系  
s a t ，  
表示状态 在动作 作用下转移到状态 的真值 其中  
s，  
，
统同时具有不确定性和模糊性 本文称这类系统为不  
［16 ～ 18］  
t
S a  
∈ 和 ∈  
Act;  
Kripke  
．
结构 例如模糊有限自动机  
．
对
确定型模糊  
( 4) AP  
是一组原子命题集合  
( 5) L: S F( AP)  
;
， ［19，20］  
于具有这类特点的系统结构 文献 分别研究了  
，L( s) ( p)  
是模糊标签函数  
表示原  
→
，
基于广义可能性结构和多值结构的模型检测 并分别  
p s  
子命题 在状态 上的真值  
．
．
给出了多项式时间的模型检测算法 在本文中将研究  
S，Act AP  
和
， M ．  
是有限集 则称 是有限的 对任  
若
Kripke CTL  
结构的  
基于任意模糊逻辑结构的不确定型  
s
S，s  
( s) = { a: S，  
t
意 ∈  
使得 δ  
NFKS  
NFKS  
的可用动作集定义为 Γ  
存在 ∈  
S，| ( s) | = 1，  
则
，
模型检测问题 并给出解决该问题的对数多项式时间  
( s，a) ( t) ＞ 0} ．  
s
若对于任意 ∈  
Γ
，
的改进算法 该研究扩展了模型检测技术在模糊系统  
Kripke  
．
结构 因此模糊  
Kripke  
结构是  
退化为模糊  
．
中的应用范围  
．
s
S， ( s)  
Γ
，
≠ 则称  
的一种特殊情形 若对任意 ∈  
2
基础知识  
M
．
，
NFKS  
是完全的 如无特别说明 本文中研究的  
均是  
: | M | = | S |  
的大小定义为  
［21］  
．
有限和完全的 有限  
NFKS M  
，
模糊集 用于刻画隶属范围不是很清楚的集合  
+
| Supp( ( s，a) ) | ．  
δ
: X  
形式化定义为 设 是一个有限论域  
，A: X ［0，1］  
是
→
∑ ∑  
s S  
∈
a
( s)  
∈Γ  
X ． x  
论域 上的模糊集 对任意 ∈  
X，A( x)  
x A  
表示 属于 的  
NFKS M  
， s S a ( s) ，  
中 对任意 ∈ 和 ∈Γ 若存在  
在
． x  
真值 若对任意 ∈  
X，A( x) { 0，1} ， A ．  
∈ 则称 为分明集  
t
S
∈ 使得 δ  
( s，a) ( t) ＞ 0，  
则称  
t
s a  
是 在动作 作用下的  
Supp( A)  
A ，  
表示模糊集 的支集 定义为  
Supp( A) = { x  
∈
．
后继状态 用  
Post( s，a) = { t S: ( s，a) ( t) ＞ 0}  
∈ δ  
表示状  
X: A( x) ＞ 0} ． Supp( A)  
若
，
是有限集 并设  
Supp( A) =  
s
a
． Pre( s) = { t S:  
态
在动作 作用下的后继状态集  
Act ( s，a) ( t) ＞ 0} s  
表示状态 的前驱状态  
∈
存
{ x ，x ，…，x } ， A = A( x ) /x + A( x ) /x + … + A  
则
1
a
在 ∈  
使得 δ  
1
2
n
1
2
2
． s  
集 一条从 状 态 出 发 的 路 径 是 一 个 无 限 序 列 ρ  
=
( x ) /x ． F( X)  
用
n
X
．
A，B  
F
∈
表示 上的所有模糊集 任意  
X，A( x) B( x) ． A = B  
当
n
s a s a …，  
1
s = s， i  
且对所有 ≥  
0
0，s  
S
a
和 ∈  
i
( X) ，A  
B
x
其中  
∈
表示对任意的 ∈  
A． ，  
为叙述方便 在这里先约定一些  
≤
0
0
1
i
( s ) ，  
使得 δ  
i
( s ，a ) ( s ) ＞ 0．  
i
( i)  
用 ρ  
A
B
B
Γ
表示路径 ρ 上的  
' = s a s a …s  
称
n
且仅当  
且
i
i + 1  
i + 1  
．
个状态 路径 ρ 的有限前缀 ρ  
． N  
0 ． I ．  
表示包含 的自然数集 表示指标集 设  
X
第
记号  
是
0
0
1
1
［22］  
． | | ， | ［0  
作有限路径片段 用 ρ 表示有限路径 ρ 的长度 即 ρ  
，f: X  
X
，
是单调函数 根据  
Tarski  
定理  
，
有限完备格  
→
…i］| = i，  
［0…i］  
( i)  
表示路径 ρ 以 ρ 为最后状态的  
其中 ρ  
f
， ． f ． f  
存在最小不动点和最大不动点 分别用 μ 和 υ 表  
． Paths( M，s)  
Paths( M) M  
分别表示 中所  
有限路径片段  
和
． X  
示 当 是非空有限集时 用  
， | X |  
X
表示集合 中元素的  
s M  
有从 出发的路径集合和 中所有路径集合  
．
．
个数  
+
NFKS M  
，
中 策略 σ  
: S  
Act :  
定义为 对任意的  
在
→
t- 、t- 、  
在模糊逻辑中运算符 模余模蕴涵 和  
+
+
s s …s S ，  
∈ 使得 σ  
n
( s s …s )  
1
( s ) ，  
其中  
n
S
S
表示  
∈Γ  
、 、  
补┑分别是经典逻辑中的合取 析取 蕴涵和否定连接  
0
1
0
n

相关下载

全部评论(0)

暂无评论
评论赚积分>>

上传资源 上传优质资源有赏金

热门标签

更多>>

最新上传

  • 打赏
  • 30日榜单

热门下载

资料专题

推荐下载

本站上的所有资源均为源于网上收集或者由用户自行上传，仅供学习和研究使用，无任何商业目的，版权归原作如有侵权，请 来信指出，本站将立即改正。

ICP许可证号：京ICP证070360号     21IC电子网 2000- 版权所有

京ICP备11013301号

京公网安备 11010802024343号