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

doi:10.3969/j.issn.0372-2112.2018.02.012

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

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

范艳焕^1,2, 李永明¹

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-huan^1,2, LI Yong-ming¹

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)

摘要/Abstract

摘要： 模糊线性时序逻辑（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

中图分类号:

TP301.2

范艳焕, 李永明. 模糊线性时序逻辑的可实现性[J]. 电子学报, 2018, 46(2): 341-346.

FAN Yan-huan, LI Yong-ming . The Realizability of Fuzzy Linear Temporal Logic[J]. Acta Electronica Sinica, 2018, 46(2): 341-346.

参考文献

[1] Christe B,Joost P K.Principles of Model Checking[M].Cambridge:The MIT Press,2008.
[2] Pnueli A,Rosner R.On the synthesis of a reactive module[A].Proceeding.POPL'89 Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages[C].New York:IEEE,1989.179-190.
[3] Almagor S,Boker U,Kupferman O.Formalizing and reasoning about quality[A].Automata,Languages,and Programming,ICALP 2013.Lecture Notes in Computer Science[C].Berlin:Springer-Verlag Berlin Heidelberg,2013.15-27.
[4] 林慧民,张文辉.模型检测:理论、方法与应用[J].电子学报,2002,36(12A):1907-1912. LIN Hui-min,ZHANG Wen-hui.Model checking:theories,techniques and applications[J].Acta Electronica Sinica,2002,36(12A):1907-1912.(in Chinese)
[5] Zadeh L A.Fuzzy Sets,Fuzzy Logic,and Fuzzy Systems[M].London:World Scientific Press,1996.
[6] Seong-ick M,Ko-Hsin L,Doheo L.Fuzzy branching temporal logic[J].IEEE Transactions on System,Man and Cybernetics,Part B (Cybernetics),2004,34(2):1045-1055.
[7] Subhankar M,Pallab D.A fuzzy real-time temporal logic[J].International Journal of Approximate Reasoning,2013,54(9):1452-1470.
[8] Pan H Y,Li Y M,Cao Y Z,Ma Z Y.Model checking fuzzy computation tree logic[J].Fuzzy Sets and Systems,2015,262(C):60-77.
[9] Li Y M.Quantitative model checking of linear-time properties based on generalized possibility measures[J].Fuzzy Sets and Systems,2017,320(C):17-39.
[10] Krzysztif R A,Erich G.Lectures in Game Theory for Computer Scientists[M].Cambridge:Cambridge University Press,2011.
[11] Erich G,Wolfgang T,Thomas W.Automata,Logics,and Infinite Games:A Guide to Current Research[M].New York:Springer-Verlag Berlin Heidelberg,2002.
[12] 李永明,李平.模糊计算理论[M].北京:科学出版社,2016.
[13] 李永明.可能LTL模型检测的两种方法[J].陕西师范大学学报,2014,42(6):21-25. LI Y M.Two methods of possibility LTL model checking[J].Journal of Shaanxi Normal University,2014,42(6):21-25.(in Chinese)
[14] Kupferman O,Lustig Y.Lattice automata[A].Verification,Model Checking,and Abstract Interpretation.VMCAI 2007.Lecture Notes in Computer Science[C].Berlin:Springer-Verlag Berlin Heidelberg,2007.199-213.
[15] Sven S.Solving parity games in big steps[J].Journal of Computer and System Sciences,2017,84(C):243-262.
[16] Pan H Y,Li Y M,Cao Y Z,Li D C.Reachability in fuzzy game graphs[J/OL].IEEE Transcations on Fuzzy Systems,http://dx.doi.org/10.1109/TFUZZ.2016.2593495,2016.
[17] Lucada,Thomas A H.Concurrent omega-regular games[A].Proceedings 15th Annual IEEE Symposium on Logic in Computer Science[C].USA:IEEE,2000.26-28.

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

The Realizability of Fuzzy Linear Temporal Logic

PDF

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 3

编辑推荐

Metrics

[1]	范艳焕, 李永明, 潘海玉. 不确定型模糊Kripke结构的计算树逻辑模型检测[J]. 电子学报, 2018, 46(1): 152-159.
[2]	梁常建, 李永明. 具有模糊时态的广义可能性线性时序逻辑的模型检测[J]. 电子学报, 2017, 45(12): 2971-2977.
[3]	梁常建, 李永明. 广义可能性计算树逻辑的模型检测问题[J]. 电子学报, 2017, 45(11): 2641-2648.