电子学报 ›› 2018, Vol. 46 ›› Issue (2): 341-346.DOI: 10.3969/j.issn.0372-2112.2018.02.012

• 学术论文 • 上一篇    下一篇

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

范艳焕1,2, 李永明1   

  1. 1. 陕西师范大学计算机科学学院, 陕西西安 710062;
    2. 青海师范大学民师院数学系, 青海西宁 810008
  • 收稿日期:2016-12-14 修回日期:2017-05-14 出版日期:2018-02-25
    • 通讯作者:
    • 李永明
    • 作者简介:
    • 范艳焕,女,1987年生于河南商丘.现为陕西师范大学计算机科学学院博士研究生.主要研究方向定量模型检测.E-mail:fan.fan1222@163.com
    • 基金资助:
    • 国家自然科学基金 (No.11671244,No.61261047); 教育部博士点基金 (No.20130202110001); 青海省自然基金项目:不确定性信息物理融合系统的可靠性计算及智能控制关键技术研究 (No.2014-ZJ-908)

The Realizability of Fuzzy Linear Temporal Logic

FAN Yan-huan1,2, LI Yong-ming1   

  1. 1. College of Computer Science, Shaanxi Normal University, Xi'an, Shaanxi 710062, China;
    2. Department of Mathematics in National Normal College, Qinghai Normal University, Xining, Qinghai 810008, China
  • Received:2016-12-14 Revised:2017-05-14 Online:2018-02-25 Published:2018-02-25
    • Corresponding author:
    • LI Yong-ming
    • Supported by:
    • National Natural Science Foundation of China (No.11671244, No.61261047); Ph.D. Programs Foundation of Ministry of Education of China (No.20130202110001); Natural Science Foundation of Qinghai Province - Key Technology Research on Reliability Calculation and Intelligent Control for Uncertainty in Cyber-Physical System (No.2014-ZJ-908)

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

关键词: 模糊线性时序逻辑, 模糊Büchi自动机, 可实现性, 模糊博弈

Abstract: 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.

Key words: fuzzy linear temporal logic, fuzzy Büchi automata, realizability, fuzzy game

中图分类号: