|
|
EDA365欢迎您登录！
您需要 登录 才可以下载或查看，没有帐号？注册
x
; ^4 r% C8 c5 D# Q3 j
摘要:本文研究了不确定型模糊Kripke结构的计算树逻辑的模型检测问题,并说明了该问题可以在对数多形式时间内解决.首先给出了不确定型模糊Kripke结构的定义,引入了模糊计算树逻辑的语法和语义.2 t: }. J, |$ C- N
. C' f, x: P8 a关键词:模型检测;计算树逻辑;模糊逻辑;Kripke结构;时态逻辑 C: Q) X- `2 j. D8 a& _
7 D- ^3 U8 {$ |: p4 \( B" ^
模型检测( model checking)的基本思想是:给定系统模型和刻画系统性质的时序逻辑,验证系统模型是否满足该公式.如果满足,则输出True;否则输出False并给出反例.其中系统模型可以由Kripke结构或迁移系统刻画.模型检测已广泛应用于计算机软硬件系统、集成电路、通信协议等方面的分析验证中.
* Q s% ^6 d l% e. W' i u% |' a: w' j% a. n/ r
! A. ~: U' C9 M. I6 |0 F
3 ~7 V6 f; X2 I% J5 k/ }/ T5 L3 B. {; | l
) B2 ^ _& ]. o9 D: V
; ^ t7 x- ~% x) a3 p9 C) H9 I
* W2 J: ~/ y$ Z5 a* R o
|
|
/1 
发表于 2021-3-24 11:10
收藏
淘帖
支持！
反对！