模糊交互时态逻辑的一些标记
|
摘要
模糊并发博弈结构是一种可以对具有模糊不确定信息的开放系统进行建模和分析的工具,基于该模型的模糊交互时态逻辑的模型检测问题初步得到解决。首先通过将模糊交互时态逻辑的模型检测问题转化为有限个经典的交互时态逻辑的模型检测问题,从而可以利用经典的交互时态逻辑的模型检测算法来解决模糊交互时态逻辑的模型检测;研究了模糊交互时态逻辑语义的连续性问题,即模糊并发博弈结构发生微小变化时,模糊交互时态逻辑的语义是否也相应地发生微小的变化。
Fuzzy concurrent game structures are a tool to model and analyze open systems with fuzzy uncertain information,and the model checking problem for fuzzy alternating-time temporal logic over these models has been explored yet.This paper first transforms model checking problem for fuzzy alternating-time temporal logic into several classical alternating-time temporal logic model checking problems,and then uses the algorithms for alternating-time temporal logic model checking problem to solve the problem.This paper also discusses the continuity property of semantics of fuzzy alternating-time temporal logic.In other words,when arbitrarily small changes happen over fuzzy concurrent game structures,small changes happen or not in truth values of fuzzy alternating-time temporal logic formulas.
Fuzzy concurrent game structures are a tool to model and analyze open systems with fuzzy uncertain information,and the model checking problem for fuzzy alternating-time temporal logic over these models has been explored yet.This paper first transforms model checking problem for fuzzy alternating-time temporal logic into several classical alternating-time temporal logic model checking problems,and then uses the algorithms for alternating-time temporal logic model checking problem to solve the problem.This paper also discusses the continuity property of semantics of fuzzy alternating-time temporal logic.In other words,when arbitrarily small changes happen over fuzzy concurrent game structures,small changes happen or not in truth values of fuzzy alternating-time temporal logic formulas.
引文
[1]Clarke E M,Grumberg O,Peled D.Model checking[M].Cambridge:MIT Press,1999.
[2]Baier C,Katoen J P.Principle of model checking[M].Cambridge:MIT Press,1999.
[3]Lin Huimin,Zhang Wenhui.Model checking:theories,techniques and applications[J].Acta Electronica Sinica,2002,30(S1):1907-1912.
[4]Chechik M,Devereux B,Gurfinkel S M.Multi-valued symbolic model-checking[J].ACM Transactions on Software Engineering and Methodology,2003,12(4):371-408.
[5]Chechik M,Gurfinkel A,Devereux B,et al.Data structures for symbolic multi-valued model-checking[J].Formal Methods in System Design,2006,29(3):295-344.
[6]Shoham S,Grumberg O.Multi-valued model checking games[J].Journal of Computer and System Sciences,2005,78(2):354-369.
[7]Meller Y,Grumberg O,Shoham S.A framework for compositional verification of multi-valued systems via abstractionrefinement[J].Information and Computation,2016,247:169-202.
[8]Zhao Lin,Wu Jinzhao.Application of Wu.s method to multivalued model checking[J].Journal of Systems Science and Mathematical Sciences,2008,28(8):1020-1029.
[9]Li Yongming,Li Lijun.Model checking of linear-time properties based on possibility measure[J].IEEE Transactions on Fuzzy Systems,2013,21(5):842-854.
[10]Li Yongming,Li Yali,Ma Zhanyou.Computation tree logic model checking based on possibility measures[J].Fuzzy Sets and Systems,2015,262:44-59.
[11]Li Yongming,Ma Zhanyou.Quantitative computation tree logic model checking based on generalized possibility measures[J].IEEE Transactions on Fuzzy Systems,2015,23(6):2034-2047.
[12]Pan Haiyu,Li Yongming,Cao Yongzhi,et al.Model checking fuzzy computation tree logic[J].Fuzzy Sets and Systems,2015,262:60-77.
[13]Pan Haiyu,Li Yongming,Cao Yongzhi,et al.Model checking computation tree logic over finite lattices[J].Theoretical Computer Science,2016,612:45-62.
[14]Yuan Hongjuan,Ma Yanfang,Pan Haiyu.Model checking for fuzzy alternating-time temporal logic[J].Computer Engineering&Science,2017,39(12):2290-2296.
[15]Alur R,Henzinger T A,Kupferman O.Alternating-time temporal logic[J].Journal of the ACM,2002,49(5):672-713.
[16]Wang Chongjun,Wu Jun,Zhang Lei,et al.On the limitation of the power of coalitional normative systems[J].Journal of Software,2012,23(7):1796-1804.
[17]Wang F,Schewe S,Huang C H.An extension of ATL with strategy interaction[J].ACM Transactions on Programming Languages and Systems,2015,37(3):9.
[18]Chen Taolue,Forejt V,Kwiatkowska M Z,et al.Automatic verification of competitive stochastic systems[J].Formal Methods in System Design,2013,43(1):61-92.
[3]林惠民,张文辉.模型检测:理论、方法与应用[J].电子学报,2002,30(S1):1907-1912.
[8]赵林,吴尽昭.基于吴方法的多值模型检验[J].系统科学与数学,2008,28(8):1020-1029.
[14]袁红娟,马艳芳,潘海玉.模糊交互时态逻辑的模型检测[J].计算机工程与科学,2017,39(12):2290-2296.
[16]王崇骏,吴骏,张雷,等.联盟规范系统及其规范能力极限[J].软件学报,2012,23(7):1796-1804.
[2]Baier C,Katoen J P.Principle of model checking[M].Cambridge:MIT Press,1999.
[3]Lin Huimin,Zhang Wenhui.Model checking:theories,techniques and applications[J].Acta Electronica Sinica,2002,30(S1):1907-1912.
[4]Chechik M,Devereux B,Gurfinkel S M.Multi-valued symbolic model-checking[J].ACM Transactions on Software Engineering and Methodology,2003,12(4):371-408.
[5]Chechik M,Gurfinkel A,Devereux B,et al.Data structures for symbolic multi-valued model-checking[J].Formal Methods in System Design,2006,29(3):295-344.
[6]Shoham S,Grumberg O.Multi-valued model checking games[J].Journal of Computer and System Sciences,2005,78(2):354-369.
[7]Meller Y,Grumberg O,Shoham S.A framework for compositional verification of multi-valued systems via abstractionrefinement[J].Information and Computation,2016,247:169-202.
[8]Zhao Lin,Wu Jinzhao.Application of Wu.s method to multivalued model checking[J].Journal of Systems Science and Mathematical Sciences,2008,28(8):1020-1029.
[9]Li Yongming,Li Lijun.Model checking of linear-time properties based on possibility measure[J].IEEE Transactions on Fuzzy Systems,2013,21(5):842-854.
[10]Li Yongming,Li Yali,Ma Zhanyou.Computation tree logic model checking based on possibility measures[J].Fuzzy Sets and Systems,2015,262:44-59.
[11]Li Yongming,Ma Zhanyou.Quantitative computation tree logic model checking based on generalized possibility measures[J].IEEE Transactions on Fuzzy Systems,2015,23(6):2034-2047.
[12]Pan Haiyu,Li Yongming,Cao Yongzhi,et al.Model checking fuzzy computation tree logic[J].Fuzzy Sets and Systems,2015,262:60-77.
[13]Pan Haiyu,Li Yongming,Cao Yongzhi,et al.Model checking computation tree logic over finite lattices[J].Theoretical Computer Science,2016,612:45-62.
[14]Yuan Hongjuan,Ma Yanfang,Pan Haiyu.Model checking for fuzzy alternating-time temporal logic[J].Computer Engineering&Science,2017,39(12):2290-2296.
[15]Alur R,Henzinger T A,Kupferman O.Alternating-time temporal logic[J].Journal of the ACM,2002,49(5):672-713.
[16]Wang Chongjun,Wu Jun,Zhang Lei,et al.On the limitation of the power of coalitional normative systems[J].Journal of Software,2012,23(7):1796-1804.
[17]Wang F,Schewe S,Huang C H.An extension of ATL with strategy interaction[J].ACM Transactions on Programming Languages and Systems,2015,37(3):9.
[18]Chen Taolue,Forejt V,Kwiatkowska M Z,et al.Automatic verification of competitive stochastic systems[J].Formal Methods in System Design,2013,43(1):61-92.
[3]林惠民,张文辉.模型检测:理论、方法与应用[J].电子学报,2002,30(S1):1907-1912.
[8]赵林,吴尽昭.基于吴方法的多值模型检验[J].系统科学与数学,2008,28(8):1020-1029.
[14]袁红娟,马艳芳,潘海玉.模糊交互时态逻辑的模型检测[J].计算机工程与科学,2017,39(12):2290-2296.
[16]王崇骏,吴骏,张雷,等.联盟规范系统及其规范能力极限[J].软件学报,2012,23(7):1796-1804.