|
EDA365欢迎您登录!
您需要 登录 才可以下载或查看,没有帐号?注册
x
5 R: x+ x7 f& w( s& `: ?摘要:模糊线性时序逻辑( fuzy linear temporal logic)被应用于刻画模糊系统的规范语言,其可实现性(realiz-ability)用于判断满足该时序逻辑公式的开放系统模型是否存在.模糊线性时序逻辑可实现性和系统合成( synthesis)的基本思想是:给定模糊线性时序逻辑公式,判断是否存在满足该公式的系统.如果存在,则构造满足该公式的最优系统.为了检验模糊线性时序逻辑的可实现性,首先引入模糊Bichi博弈的定义,作为检验模糊线性时序逻辑公式是否可实现的模型.其次通过归约的方法,研究模糊Bichi博弈的性质(最优无记忆策略存在性.最后验证模糊线性时序逻辑的可实现性并且给出其系统合成的过程,并说明它们的时间复杂度.: M0 ^. f6 `* x! [/ @
6 G5 q& i! I' D关键词:模糊线性时序逻辑;模糊Buichi自动机;可实现性;模糊博弈% h' l( B8 |+ l8 y/ m8 q0 P
( N. n. W h4 I6 e+ m4 I 模型检测(model checking)技术是用于检验系统是否满足期望的属性.系统合成是给定属性(可以用时序逻辑刻画),自动地构造一个满足该属性的系统.在系统合成的过程中,时序逻辑( temporal logic)的可实现性的基本思想是已知属性(用时序逻辑公式表示),判断满足属性的系统是否存在.如果存在,则称时序逻辑公式是可实现的.. \0 L9 o# n' n: ^
$ }% H$ X! T) W" U1 A0 z# G* a1 `4 h6 A* W5 [& P: e
* ]& o- p. q( n+ @
7 J9 z$ E5 X7 U; b) u% w
0 y1 {4 T( m4 @$ J8 q% _3 f' z0 `4 @7 a/ m
0 W: L( E/ j6 J) H6 ^6 Y
|
|