不确定型模糊Kripke结构的计算树逻辑模型检测

本文研究了不确定型模糊Kripke结构的计算树逻辑的模型检测问题,并说明了该问题可以在对数多形式时间内解决.首先给出了不确定型模糊Kripke结构的定义,引入了模糊计算树逻辑的语法和语义.为了刻画存在量词∃和任意量词∀在不确定型模糊Kripke结构中的两种语义解释,在模糊计算树逻辑语法中引入了路径量词∃_sup,∃_inf和∀_sup,∀_inf,分别用于替换存在量词∃和任意量词∀.其次讨论了基于不确定型模糊Kripke结构的计算树逻辑模型检测算法,特别地对于模糊计算树逻辑公式∃_suppUq,∀_suppUq,∃_infpUq和∀_infpUq分别给出时间复杂度为对数多项式时间的改进算法.     

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

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