|
|
EDA365欢迎您登录！
您需要 登录 才可以下载或查看，没有帐号？注册
x
6 }+ G) z/ S% g9 Z3 |- o摘要:本文研究了不确定型模糊Kripke结构的计算树逻辑的模型检测问题,并说明了该问题可以在对数多形式时间内解决.首先给出了不确定型模糊Kripke结构的定义,引入了模糊计算树逻辑的语法和语义.* c% n% ^; p% y; Q. j+ |' a4 m6 c
' u( p: B8 ^# x4 o4 r
关键词:模型检测;计算树逻辑;模糊逻辑;Kripke结构;时态逻辑
; }6 q& B& _6 [* j- y" m; d# o1 `- ]$ t6 Y& C7 P
模型检测( model checking)的基本思想是:给定系统模型和刻画系统性质的时序逻辑,验证系统模型是否满足该公式.如果满足,则输出True;否则输出False并给出反例.其中系统模型可以由Kripke结构或迁移系统刻画.模型检测已广泛应用于计算机软硬件系统、集成电路、通信协议等方面的分析验证中.1 g# s# P( U3 h: J9 f& C4 o
( z' `/ P" M1 a6 C& a/ l" x2 X
1 g+ f" h. W# z
. { ^% K1 N6 z' w
' f& ^6 J2 k y3 M
% S1 \2 x. u- V6 f% A( d) K6 W9 T. E; j. \! h- |$ P) @
6 B+ Q% b/ d* b I |
|
/1 
发表于 2021-3-24 11:10
收藏
淘帖
支持！
反对！