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

模糊线性时序逻辑（fuzzy linear temporal logic）被应用于刻画模糊系统的规范语言，其可实现性（realizability）用于判断满足该时序逻辑公式的开放系统模型是否存在.模糊线性时序逻辑可实现性和系统合成（synthesis）的基本思想是：给定模糊线性时序逻辑公式，判断是否存在满足该公式的系统.如果存在，则构造满足该公式的最优系统.为了检验模糊线性时序逻辑的可实现性，首先引入模糊Büchi博弈的定义，作为检验模糊线性时序逻辑公式是否可实现的模型.其次通过归约的方法，研究模糊Büchi博弈的性质（最优无记忆策略存在性.最后验证模糊线性时序逻辑的可实现性并且给出其系统合成的过程，并说明它们的时间复杂度.

The Realizability of Fuzzy Linear Temporal Logic

FLTL(Fuzzy Linear Temporal Logic) is used as the specification language of fuzzy system,the realizability focuses on judging whether there exists the model for open system satisfying the FLTL formulea.the basic idea of FLTL realizability and synthesis problem is as follow:given a specification,verifying whether there exists a system whose truth value of satisfying the specification is greater than zero.If existed,then we call FLTL formulae described the specification is realizable.First,fuzzy game graph with Büchi objective was proposed,which is used as the model to verify whether FLTL is realizable.Second,we studied the property of fuzzy game graph with Büchi objective by the method of reduction.Last,realizability of fuzzy linear temporal logic was studied and the procedure of system synthesis was given,their time complexities were analyzed.