|
|
EDA365欢迎您登录！
您需要 登录 才可以下载或查看，没有帐号？注册
x
2 n) g B5 M0 V S- J
摘要:本文研究了不确定型模糊Kripke结构的计算树逻辑的模型检测问题,并说明了该问题可以在对数多形式时间内解决.首先给出了不确定型模糊Kripke结构的定义,引入了模糊计算树逻辑的语法和语义.9 n& h- s: u8 Y" A& q) [
% c9 M0 _9 v7 ~5 G6 [9 Z) B) w
关键词:模型检测;计算树逻辑;模糊逻辑;Kripke结构;时态逻辑% \% T; X& i3 Q- [% R- ^4 W# J
1 P: V! a8 j# C6 D 模型检测( model checking)的基本思想是:给定系统模型和刻画系统性质的时序逻辑,验证系统模型是否满足该公式.如果满足,则输出True;否则输出False并给出反例.其中系统模型可以由Kripke结构或迁移系统刻画.模型检测已广泛应用于计算机软硬件系统、集成电路、通信协议等方面的分析验证中.3 h; m v; D# b- a. I
1 ^' [6 R! O5 W4 j0 R/ z9 V- h- u+ A; t
2 M a# t& ]4 h: L2 x. t2 p. x3 v! u7 o$ L
6 L* e) Q& W6 I2 z! s% ]
. R) N, c! s2 R# w
; y( y& r, b: `8 m |
|
/1 
发表于 2021-3-24 11:10
收藏
淘帖
支持！
反对！