|
|
EDA365欢迎您登录！
您需要 登录 才可以下载或查看，没有帐号？注册
x
?+ L! | _# q( y$ S摘要:本文研究了不确定型模糊Kripke结构的计算树逻辑的模型检测问题,并说明了该问题可以在对数多形式时间内解决.首先给出了不确定型模糊Kripke结构的定义,引入了模糊计算树逻辑的语法和语义.
7 ^, A8 p1 u* I5 j0 f& o0 E3 V; V) S3 l
关键词:模型检测;计算树逻辑;模糊逻辑;Kripke结构;时态逻辑
3 d% F1 A5 q6 \7 k0 |2 e J/ t: m9 Z- s$ `% p
模型检测( model checking)的基本思想是:给定系统模型和刻画系统性质的时序逻辑,验证系统模型是否满足该公式.如果满足,则输出True;否则输出False并给出反例.其中系统模型可以由Kripke结构或迁移系统刻画.模型检测已广泛应用于计算机软硬件系统、集成电路、通信协议等方面的分析验证中.
7 z1 S7 y$ ^! L* r3 e1 j
; s- l* T# C' r+ O% z* r* a& }% J# `7 {2 S; b8 ?
0 P- E6 O! Z* I8 Z1 r0 n# q& F% l% B& o, B5 [
+ d: i7 r; \$ R* ~2 I# ~
9 |1 ?3 L9 o }1 q
' ~5 t4 i* ~# b2 H0 I Y- O- P; M, q |
|
/1 
发表于 2021-3-24 11:10
收藏
淘帖
支持！
反对！