|
|
EDA365欢迎您登录！
您需要 登录 才可以下载或查看，没有帐号？注册
x
5 b7 y8 ^0 |$ c% x9 Z
摘要:本文研究了不确定型模糊Kripke结构的计算树逻辑的模型检测问题,并说明了该问题可以在对数多形式时间内解决.首先给出了不确定型模糊Kripke结构的定义,引入了模糊计算树逻辑的语法和语义.7 S( U8 o8 `8 T! K' \0 a
/ D6 H4 V; R4 C4 k9 `
关键词:模型检测;计算树逻辑;模糊逻辑;Kripke结构;时态逻辑1 H. S6 g% q+ @8 M% y1 u
. ?2 |9 F3 W6 B5 [- R
模型检测( model checking)的基本思想是:给定系统模型和刻画系统性质的时序逻辑,验证系统模型是否满足该公式.如果满足,则输出True;否则输出False并给出反例.其中系统模型可以由Kripke结构或迁移系统刻画.模型检测已广泛应用于计算机软硬件系统、集成电路、通信协议等方面的分析验证中.
# [: i6 H( j3 h P6 l5 D. p7 ^/ Z [1 M# |, x: x! e C
( `7 e7 v& Q" t1 ^! H7 S0 n* d" v, Y0 a' P" b
; L! G/ G' `1 B$ b* |3 U- d8 N
! a/ Q" l( |; K3 N! ]/ J" f7 Y) r
$ W2 ?; Z4 }2 h& o( E7 [ |
|
/1 
发表于 2021-3-24 11:10
收藏
淘帖
支持！
反对！