推荐星级：
- 1
- 2
- 3
- 4
- 5
不确定型模糊Kripke结构的计算树逻辑模型检测
资料介绍
本文研究了不确定型模糊Kripke结构的计算树逻辑的模型检测问题,并说明了该问题可以在对数多形式时间内解决.首先给出了不确定型模糊Kripke结构的定义,引入了模糊计算树逻辑的语法和语义.为了刻画存在量词?和任意量词在不确定型模糊Kripke结构中的两种语义解释,在模糊计算树逻辑语法中引入了路径量词?sup,?inf和sup,inf,分别用于替换存在量词?和任意量词.其次讨论了基于不确定型模糊Kripke结构的计算树逻辑模型检测算法,特别地对于模糊计算树逻辑公式?suppUq,suppUq,?infpUq和infpUq分别给出时间复杂度为对数多项式时间的改进算法.
部分文件列表
| 文件名 | 大小 |
| 不确定型模糊Kripke结构的计算树逻辑模型检测.pdf | 1M |
部分页面预览
（完整内容请下载后查看）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
更多>>
最新上传
- 打赏
- 30日榜单
-
21ic小能手 打赏10.00元 3天前
-
21ic小能手 打赏10.00元 3天前
-
21ic小能手 打赏10.00元 3天前
-
21ic下载 打赏310.00元 3天前
用户：小猫做电路
-
21ic下载 打赏310.00元 3天前
用户：gsy幸运
-
21ic下载 打赏310.00元 3天前
用户：liqiang9090
-
21ic下载 打赏310.00元 3天前
用户：zhengdai
-
21ic下载 打赏160.00元 3天前
用户：w1966891335
-
21ic下载 打赏160.00元 3天前
用户：w178191520
-
21ic下载 打赏160.00元 3天前
用户：kk1957135547
-
21ic下载 打赏40.00元 3天前
用户：WK520077778
-
21ic下载 打赏40.00元 3天前
用户：sun2152
-
21ic下载 打赏30.00元 3天前
用户：xuzhen1
-
21ic下载 打赏50.00元 3天前
用户：铁蛋锅
-
21ic下载 打赏30.00元 3天前
用户：xzxbybd
-
21ic下载 打赏40.00元 3天前
用户：z00
-
21ic下载 打赏40.00元 3天前
用户：forgot
-
21ic下载 打赏40.00元 3天前
用户：happypcb
-
21ic下载 打赏20.00元 3天前
用户：zhaoqshan
-
21ic下载 打赏5.00元 3天前
用户：17724187683
-
21ic下载 打赏5.00元 3天前
用户：zmm1818
-
21ic小能手 打赏15.00元 3天前
-
21ic小能手 打赏5.00元 3天前
-
21ic小能手 打赏5.00元 3天前
-
chenruiji 打赏1.00元 3天前
资料：血糖仪原理图
-
21ic小能手 打赏5.00元 3天前
-
21ic小能手 打赏5.00元 3天前
-
21ic小能手 打赏5.00元 3天前
-
21ic小能手 打赏10.00元 3天前
-
21ic小能手 打赏5.00元 3天前
-
21ic小能手 打赏10.00元 3天前
-
21ic小能手 打赏5.00元 3天前
-
21ic小能手 打赏5.00元 3天前
-
21ic小能手 打赏5.00元 3天前
资料：测试智能语音控制模块
-
21ic小能手 打赏5.00元 3天前
-
21ic小能手 打赏5.00元 3天前
-
21ic小能手 打赏10.00元 3天前
-
21ic小能手 打赏10.00元 3天前
-
cai0603 打赏3.00元 3天前
用户：CJQ_ENJOY
-
21ic小能手 打赏5.00元 3天前
全部评论(0)