推荐星级：
- 1
- 2
- 3
- 4
- 5
具有模糊时态的广义可能性线性时序逻辑的模型检测
资料介绍
本文首先定义了具有模糊时态的广义可能性线性时序逻辑GPoFLTL(Generalized Possibilistic Fuzzy Linear Tempora Logic)的语构以及基于路径和基于语言的两种语义解释,证明了GPoFLTL在模糊时态方面对GPo LTL(Generalized Possibilistic Linear Tempora Logic)进行了扩张,并通过实例说明了GPoFLTL比GPo LTL具有更强的表达能力;其次在广义可能性测度下通过模糊矩阵运算讨论了“不久”,“几乎总是”等几类模糊时态性质的模型检测问题;最后研究了模糊时态性质的必要性阈值模型检测问题,给出了基于自动机的GPoFLTL的阈值模型检测算法及算法的复杂度.
部分文件列表
| 文件名 | 大小 |
| 具有模糊时态的广义可能性线性时序逻辑的模型检测.pdf | 1M |
部分页面预览
（完整内容请下载后查看）12
Vol． 45 No． 12
Dec． 2017
第
期
电
子
学
报
2017
12
ACTA ELECTRONICA SINICA
年
月
具有模糊时态的广义可能性
线性时序逻辑的模型检测
1，2
1
，
梁常建 李永明
( 1．
，
陕西师范大学数学与信息科学学院 陕西西安
710119; 2．
，
商丘师范学院数学与统计学院 河南商丘
476000)
:
GPoFLTL( Generalized Possibilistic Fuzzy
摘
要
本文首先定义了具有模糊时态的广义可能性线性时序逻辑
Linear Tempora Logic)
，
的语构以及基于路径和基于语言的两种语义解释 证明了
GPoFLTL
GPoLTL
在模糊时态方面对
GPoLTL
具有更强的表达能
( Generalized Possibilistic Linear Tempora Logic) ， GPoFLTL
进行了扩张 并通过实例说明了
比
; “ ”，“ ” ;
力 其次在广义可能性测度下通过模糊矩阵运算讨论了 不久 几乎总是 等几类模糊时态性质的模型检测问题
，
最后研究了模糊时态性质的必要性阈值模型检测问题 给出了基于自动机的
GPoFLTL
的阈值模型检测算法及算法的
．
复杂度
关键词
中图分类号
URL: http: / /www． ejournal． org． cn
:
;
;
;
;
模糊时态 可能性性质 线性时序逻辑 时间复杂度 阈值模型检测
TP301. 2 0372-2112 ( 2017) 12-2971-07
DOI: 10． 3969 /j． issn． 0372-2112． 2017． 12． 020
:
:
A
:
文章编号
文献标识码
电子学报
Model Checking of Fuzzy Linear Temporal Logic
Based on Generalized Possibility Measures
1，2
1
LIANG Chang-jian ，LI Yong-ming
( 1． School of Mathematics and Information Science，Shaanxi Normal University，Xi’an，Shaanxi 710119，China;
2． School of Mathematics and Statistics，Shangqiu Normal University，Shangqiu，Henan 476000，China)
Abstract: In this paper，firstly，the syntax and semantics of GPoFLTL( Generalized Possibilistic Fuzzy Linear Tempo-
ra Logic) are given，especially，both the path and language semantics of GPoFLTL are discussed． It is shown that GPoFLTL
is the extension to GPoLTL( Generalized Possibilistic Linear Tempora Logic) with respect to fuzzy time，and that GPoFLTL
has the stronger expression power than GPoLTL illustrated by some examples． Secondly，GPoFLTL model checking based on
the generalized possibility measures is discussed using fuzzy matrix operator，which includes some fuzzy time temporal，
“Soon”，“Nearly always”，etc． Finally，the necessity threshold model checking problem of fuzzy linear time properties with
fuzzy time temporal is studied; furthermore，the algorithm of the necessity threshold model checking of GPoFLTL based on
automata method is given，and the time complexity of this method is proved．
Key words:
fuzzy time temporal; possibility property; linear temporal logic; time complexity; threshold
model checking
［4，5］
、
理论的多值模型检测
基于模糊逻辑的模糊模型检
1
引言
［6，7］
［8］
CTL
．
，
特别地
测
以及基于格值逻辑的
模型检测
［1，2］
经典的模型检测
方法已经不能处理正确性要
，
为了处理不满足概率测度可加性的不确定现象 李永
［9］
， 、
求较高的系统中的不确定性信息 为了有效的处理 刻
，
Kripke
结
明等基于可能性理论
定义了广义可能性
［10 ～ 13］
，
画这些不确定性 人们研究了基于概率测度的随机模
( GPKS)
， ，
在其 上 引入 了可 能 性 测 度 研究 了
构
［1］
［3］
、 、
基于量子理论的量子 模型检测 基于多值
型检测
GPoLTL(
)
广义可能性线性时序逻辑 和
GPoCTL(
广义可
: 2016-12-11 ;
: 2017-03-23; :
责任编辑 梅志强
收稿日期
修回日期
:
基金项目 国家自然科学基金
( No． 11271237，No． 11671244，No． 11401363，No． 11501345) ;
( No．
高等学校博士学科点专项科研基金项目
20130202110001)
2972
2017
年
电
子
学
报
) ．
能性计算树逻辑 及其对应的模型检测 相对于多值
、
L( s) ( a)
s a
表示状态 满足命题 的可能性
．
用
， ［12，13］ ，
模糊时序逻辑 文献 引入广义可能性测度 使
S
AP
，
M
GPKS．
如果
本文讨论的
可能性状态转移分布函数
和
都是有限的 则称 是有限的
; ，
时态性质可度量化 相对于随机模型检测 文献
［12，
GPKS
．
都是有限的
13］
处理的是满足可能性测度的现象而不是满足概率
P: S × S ［0，1］
可以用
→
． ， 、
测度可加性的现象 然而 多值 可能性时态逻辑等相对
P ，
一个模糊矩阵 来表示 其中
P = ( P( s，t) )
． P
的传
s，t
∈
S
+
+
2
于经典的时态逻辑只是对布尔连接词和命题的模糊
P ．
S
N
， P = P
个状态 则
P
∨ ∨
递闭包记作
若集合
有
N
k + 1
k
， ， “ ”、“
化 时态表示却是经典的 对于具有 不久 几乎总
…
P ， k
其中 ≥
0，P
= P P，(
， ，
分别用符号∨ ∧
∨
” ． ，
是 等模糊时间性质的模糊时态并未讨论 例如 观察
，
在逻辑公式的运算中表示逻辑析取 逻辑合取和逻
，
某学生上课的注意力是否是集中的 由于人的集中力
;
辑非 在逻辑公式的赋值运算表示模糊集中的实数区
，
持续时间有限 因此要求在学生上课时间一直不中断
［0，1］ ， ) ．
间 上的取大运算 取小运算和否定运算
，
的集中精力听讲是不可能的 所以也就只能观察学生
GPKS M
， s
而言 从状态 出发的一条路径
对于一个
“ ” ，
在上课时间注意力 几乎总是 集中的情形 这种情况
， :
π 用一组无限的状态序列表示 即
= s s …， s
其中
1
π
0
0
．
用经典的时态连接词无法表示
为了量化处理这些具有模糊时间性质且不满足概
= s， i P( s ，s ) ＞ 0． P ( s)
0，
且对于任意的 ≥ 都有 表
aths
i
i + 1
s
． P ( M) =
示从状态 出发的所有路径组成的集合
( s ) ． tr( ) = L( s ) L( s ) …，
也
aths
， ［13］
率可加性的不确定性现象 本文结合文献 和文献
P
∪
路径 π 对应的迹
π
aths
0
0
1
s
I
∈
0
［14］， ，
基于可能性测度 在
GPKS
，
下 定义了
GPoFLTL
L( ) ， L( ) = L( s ) L( s ) … ， Trs( ) =
π
可记为
{ tr( ) |
π
π
即
记
∏
0
1
(
)
具有模糊时态的广义可能性线性时序逻辑 的语构以
} ，Trs( s) = Trs( P ( s) ) ． M
aths
M
中
π∈∏
的值为
． ［13］
及基于路径和语言的两种语义 本文与文献 不同
，
的状态 数 与 转 移 个 数 之 和 记 为
| M | ， : | M | =
即
，
之处是引入了模糊时态算子 模糊时态算子的模糊语
| Supp( P) | + | S | ．
［9］
X
，
义与模糊理论中的模糊隶属函数不同 这里的模糊是
2
X
设
， = 2 ，
是一个非空集合 Ω 若函数
定义
，
由于延迟或忽略的时刻数的不确定性引起的 针对这
Me:
［0，1］ : ( 1) Me( ) = 0; ( 2)
满足条件 对任意的
→
Ω
，
种不确定性引入了惩罚函数 表示对延迟或忽略的时
E
，i I，Me(
∈Ω ∈
E ) =
i
Me( E ) ， Me
则称 是 Ω 上
i
∪
∨
i
i
I
i
I
∈
∈
，
刻数进行惩罚的程度 而惩罚函数的选择则根据经验
．
的广义可能性测度
，
，
GPoFLTL
而得 并且通过具体的实例分析 说明了
可以
”、“ GPoLTL
解决具有像 不久 几乎总是 等 无法很好
［12，13］
M
3
M
是一个
GPKS， Po :
定义映射
定义
( M)
设
“
”
P
［0，1 ］， = s s …， :
对 任 意 的 路 径 π 有
0 1
→
aths
． ［14］
地表达的具有模糊时间的性质 文献 仅仅讨论了
∞
M
Po ( ) = I( s )
π
0
P( s ，s ) ． E P
若对
aths
( M) ，
定义
∧∧
i
i + 1
，
模糊时态连接词及连接词之间的关系 并且给出具体
i = 0
M
M
M
Po ( E) = { Po ( ) |
∨ π π∈
E} ， Po :
则可得扩张映射
，
有效的例子较少 找到研究模型检测问题的切入点也
Paths( M)
M
2
［0，1］，
易知
→
Po
．
是 Ω 上的广义可能性测度
，
比较困难 相关的模型检测问题及其算法研究也就未
［12］
1
M
是一个
GPKS， r : S ［0，1］
映射
→
命题
设
; ［14］， ，
讨论 相对于文献 本文引入了广义可能性测度
P
: r ( s) = { P( s，s ) P( s ，s ) … | ss s …
∨ ∧ ∧ ∈
2
定义为
，
在广义可能性测度下研究具有模糊时间性质的现象
P
1
1
1 2
+
+
P
( M) } ， s S，
其中 ∈ 则有
r ( s) = { P ( s，t)
∨
P
P
∧
;
通过实际现象对模糊时态词进行了合适的解释 且在
aths
( t，t) | t S} ．
∈
广义可能性测度意义下讨论模糊时态算子的模型检测
［13］ ，GPoLTL
文献 中 只是对布尔连接词和命题进
，
和阈值模型检测问题 给出了基于自动机的
GPoFLTL
，
行了模糊化 对具有模糊时间性质的模糊时态却无法
．
模型检测问题的算法及其复杂度
t
≤
． ， GPoLTL
表示 例如 在
，
中 □
Q
t Q
表示在 时间内 是
2
基本概念与性质
， Q t
一直发生的 如果 在 时间内的某些不确定时刻不发
［16，17］
t
≤
1
Kripke
( Gen-
定义
eralized Possibilistic Kripke Structure，GPKS) M = ( S，P，
I，AP，L)
一个广义的可能性
结构
(
生 或发生的程度为
0) ，
‖□
Q
(
‖ σ
) = 0， ，GPo-
因此
LTL
“ ” Q
不能表示像 几乎总是 这种具有允许 在某些时
，
:
是一个五元组 其中
．
刻不发生的模糊时态 为了处理这些具有模糊时间性
( 1) S
;
是一个可数的非空状态集
，
质的不确定现象 扩充
GPoLTL
在模糊时态方面的表达
( 2) P: S × S ［0，1］
→
;
，
能力 下面给出具有模糊时态的广义可能性线性时序
是可能性状态转移分布函数
( 3) I: S ［0，1］
→
;
．
是可能性初始状态分布函数
逻辑的语构及语义解释
( 4) AP
;
4
是一个原子命题集合
定义
具有模糊时态的广义可能性线性时序逻
AP
( 5) L: S ［0，1］
→
，
是可能性标签函数 该函数为每
( Generalized Possibilistic Fuzzy Linear Temporal Logic，
辑
，
个状态赋一个原子命题的模糊集 其中对
a
∈
AP，s S，
∈
GPoFLTL)
:
的语构按如下方式递归定义
更多>>
最新上传
- 打赏
- 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)