|
EDA365欢迎您登录!
您需要 登录 才可以下载或查看,没有帐号?注册
x
- Z7 q1 t) T/ j ~
摘要:模糊线性时序逻辑( fuzy linear temporal logic)被应用于刻画模糊系统的规范语言,其可实现性(realiz-ability)用于判断满足该时序逻辑公式的开放系统模型是否存在.模糊线性时序逻辑可实现性和系统合成( synthesis)的基本思想是:给定模糊线性时序逻辑公式,判断是否存在满足该公式的系统.如果存在,则构造满足该公式的最优系统.为了检验模糊线性时序逻辑的可实现性,首先引入模糊Bichi博弈的定义,作为检验模糊线性时序逻辑公式是否可实现的模型.其次通过归约的方法,研究模糊Bichi博弈的性质(最优无记忆策略存在性.最后验证模糊线性时序逻辑的可实现性并且给出其系统合成的过程,并说明它们的时间复杂度.1 m, A9 w* K7 ]0 B' w" z7 w
3 Y( L- j% G; f. N1 L3 O关键词:模糊线性时序逻辑;模糊Buichi自动机;可实现性;模糊博弈
7 A3 L! o, `9 z4 u3 k' h6 e" o! u
模型检测(model checking)技术是用于检验系统是否满足期望的属性.系统合成是给定属性(可以用时序逻辑刻画),自动地构造一个满足该属性的系统.在系统合成的过程中,时序逻辑( temporal logic)的可实现性的基本思想是已知属性(用时序逻辑公式表示),判断满足属性的系统是否存在.如果存在,则称时序逻辑公式是可实现的.
6 h1 ]6 k) C4 H4 I' s4 B1 ?; c
5 B' {/ l, i# k# N& V
/ ] Y# r: ]1 Q, N( J# B3 ~. {. m0 g
& `6 h! U( q/ k7 ^9 P; a2 j
2 T! @% P Z+ h: N, V& ^' h0 e1 G: d# `4 I% X& O
' u u: ^" ?8 f0 h( ~, m5 X$ _ |
|