|
EDA365欢迎您登录!
您需要 登录 才可以下载或查看,没有帐号?注册
x
' G( j B2 i% o7 g2 ~2 e1 h
摘要:模糊线性时序逻辑( fuzy linear temporal logic)被应用于刻画模糊系统的规范语言,其可实现性(realiz-ability)用于判断满足该时序逻辑公式的开放系统模型是否存在.模糊线性时序逻辑可实现性和系统合成( synthesis)的基本思想是:给定模糊线性时序逻辑公式,判断是否存在满足该公式的系统.如果存在,则构造满足该公式的最优系统.为了检验模糊线性时序逻辑的可实现性,首先引入模糊Bichi博弈的定义,作为检验模糊线性时序逻辑公式是否可实现的模型.其次通过归约的方法,研究模糊Bichi博弈的性质(最优无记忆策略存在性.最后验证模糊线性时序逻辑的可实现性并且给出其系统合成的过程,并说明它们的时间复杂度.! t1 F, m7 u( q9 F+ A) U& F3 u
5 {+ \, O1 @, L7 n+ C4 B% g关键词:模糊线性时序逻辑;模糊Buichi自动机;可实现性;模糊博弈
9 k1 n+ b: _6 u- d, D5 f5 V: i2 E1 }
模型检测(model checking)技术是用于检验系统是否满足期望的属性.系统合成是给定属性(可以用时序逻辑刻画),自动地构造一个满足该属性的系统.在系统合成的过程中,时序逻辑( temporal logic)的可实现性的基本思想是已知属性(用时序逻辑公式表示),判断满足属性的系统是否存在.如果存在,则称时序逻辑公式是可实现的.2 W* T% ^* R/ i. e/ C2 \
! j! L, Y# O* u
; ^, n+ M0 B6 T1 f) Q! y U! h& Q( _" X0 |2 ]' d- l
S/ N- c, W/ N6 e; Y1 y
# Q) B, ^+ l# q3 j
1 a' F) [5 M# u- B" `, A7 l( ?: W( e1 r: p
|
|