|
|
EDA365欢迎您登录！
您需要 登录 才可以下载或查看，没有帐号？注册
x
) C6 Y, W+ P& g摘要:本文研究了不确定型模糊Kripke结构的计算树逻辑的模型检测问题,并说明了该问题可以在对数多形式时间内解决.首先给出了不确定型模糊Kripke结构的定义,引入了模糊计算树逻辑的语法和语义.
& R! O6 U$ r$ I7 h, m) e. F0 k) ?9 q% i( P
关键词:模型检测;计算树逻辑;模糊逻辑;Kripke结构;时态逻辑6 S# v" L, Q1 j# ^5 ~+ @; Z L
: W8 J7 q+ p* \# K* d G9 u 模型检测( model checking)的基本思想是:给定系统模型和刻画系统性质的时序逻辑,验证系统模型是否满足该公式.如果满足,则输出True;否则输出False并给出反例.其中系统模型可以由Kripke结构或迁移系统刻画.模型检测已广泛应用于计算机软硬件系统、集成电路、通信协议等方面的分析验证中.
3 `5 {4 ]$ W( g6 Q# g. j) W, H# l0 n$ {$ C. A' L3 B+ L5 p
2 m8 A) e$ U5 e* i$ B5 {
) m! j" x: O6 N1 C
; m4 p. Z* c6 U+ q' i* b
6 w1 d3 |5 {- x* b/ I d- B2 R# f8 X3 z
( n1 H( E% @1 h8 n0 N3 F4 ^: j |
|
/1 
发表于 2021-3-24 11:10
收藏
淘帖
支持！
反对！