|
|
EDA365欢迎您登录！
您需要 登录 才可以下载或查看，没有帐号？注册
x
! ?7 [* s% p/ ]7 b3 B+ O+ B8 a
摘要:本文研究了不确定型模糊Kripke结构的计算树逻辑的模型检测问题,并说明了该问题可以在对数多形式时间内解决.首先给出了不确定型模糊Kripke结构的定义,引入了模糊计算树逻辑的语法和语义.
# v' u8 X" H8 x5 i! m2 R4 H+ q; z( ?! J4 K8 E: ]
关键词:模型检测;计算树逻辑;模糊逻辑;Kripke结构;时态逻辑% c& V6 N+ m' Y4 x q+ W( |
: @+ |+ ?0 [3 [! j3 R; W
模型检测( model checking)的基本思想是:给定系统模型和刻画系统性质的时序逻辑,验证系统模型是否满足该公式.如果满足,则输出True;否则输出False并给出反例.其中系统模型可以由Kripke结构或迁移系统刻画.模型检测已广泛应用于计算机软硬件系统、集成电路、通信协议等方面的分析验证中.& ?& B- ?2 @" A- `# M, U! b
3 H! S; d: r# V4 z8 l( r
9 M7 o4 W- s8 M; e9 ^% n4 E2 ]3 V4 z
2 U. }6 [- v5 w# c% ^. i% B" F$ Q9 d
8 l) F2 I+ M, J, _8 s1 l! o7 X
8 d, v, \ \8 s$ U" u
2 |1 W" F9 e) m& P: t \ |
|
/1 
发表于 2021-3-24 11:10
收藏
淘帖
支持！
反对！