模糊线性时序逻辑的可实现性

zxshunine

摘要:模糊线性时序逻辑( fuzy linear temporal logic)被应用于刻画模糊系统的规范语言,其可实现性(realiz-ability)用于判断满足该时序逻辑公式的开放系统模型是否存在.模糊线性时序逻辑可实现性和系统合成( synthesis)的基本思想是:给定模糊线性时序逻辑公式,判断是否存在满足该公式的系统.如果存在,则构造满足该公式的最优系统.为了检验模糊线性时序逻辑的可实现性,首先引入模糊Bichi博弈的定义,作为检验模糊线性时序逻辑公式是否可实现的模型.其次通过归约的方法,研究模糊Bichi博弈的性质(最优无记忆策略存在性.最后验证模糊线性时序逻辑的可实现性并且给出其系统合成的过程,并说明它们的时间复杂度.
* [: S, z4 T8 U7 ^
' W& {. P# I0 v关键词:模糊线性时序逻辑;模糊Buichi自动机;可实现性;模糊博弈
- M) w# r9 e2 s! E5 h* l
. s& r, C7 p6 n) n. ]       模型检测(model checking)技术是用于检验系统是否满足期望的属性.系统合成是给定属性(可以用时序逻辑刻画),自动地构造一个满足该属性的系统.在系统合成的过程中,时序逻辑( temporal logic)的可实现性的基本思想是已知属性(用时序逻辑公式表示),判断满足属性的系统是否存在.如果存在,则称时序逻辑公式是可实现的.


1 h, r; h0 ~* A( Z- d

游客，如果您要查看本帖隐藏内容请回复

* {( J: a2 ?9 l# U
1 J# Y: B1 ]8 P3 @) X$ U6 E
" Z5 b  C- J1 j# f1 o
$ i% A4 `, {2 f" x9 v
+ [3 }8 x6 d. _

nevadaooo

模型检测技术是用于检验系统是否满足期望的属性