|
EDA365欢迎您登录!
您需要 登录 才可以下载或查看,没有帐号?注册
x
9 }# a' Z- w: Q: W J% M8 h摘要:模糊线性时序逻辑( fuzy linear temporal logic)被应用于刻画模糊系统的规范语言,其可实现性(realiz-ability)用于判断满足该时序逻辑公式的开放系统模型是否存在.模糊线性时序逻辑可实现性和系统合成( synthesis)的基本思想是:给定模糊线性时序逻辑公式,判断是否存在满足该公式的系统.如果存在,则构造满足该公式的最优系统.为了检验模糊线性时序逻辑的可实现性,首先引入模糊Bichi博弈的定义,作为检验模糊线性时序逻辑公式是否可实现的模型.其次通过归约的方法,研究模糊Bichi博弈的性质(最优无记忆策略存在性.最后验证模糊线性时序逻辑的可实现性并且给出其系统合成的过程,并说明它们的时间复杂度.7 K& B1 W' c4 N+ }
& T$ W( T* l8 t6 O/ x9 i# @关键词:模糊线性时序逻辑;模糊Buichi自动机;可实现性;模糊博弈, ]/ ]6 T# l1 j
; b2 U. U0 p. U3 y5 }8 U 模型检测(model checking)技术是用于检验系统是否满足期望的属性.系统合成是给定属性(可以用时序逻辑刻画),自动地构造一个满足该属性的系统.在系统合成的过程中,时序逻辑( temporal logic)的可实现性的基本思想是已知属性(用时序逻辑公式表示),判断满足属性的系统是否存在.如果存在,则称时序逻辑公式是可实现的.
1 N# o* |1 B3 r' ]+ i" f$ t! ?% n! \
- M, q/ |) Y) m1 G; N
# m4 n- O* L$ C- L% P4 T9 r- G; Z3 L, _
5 u T' |& C, \0 \! E( f; `; f
* X$ ~. o" }( Z5 Q3 c$ ?
. C& R! ]- [8 |2 O, A |
|