摘要： 根据初始状态、状态之间的转换关系和命题赋值函数是否为分明的,模糊Kripke结构可分为8类。提出将模糊计算树逻辑作为判断模糊Kripke结构之间是否是等价的依据；详细讨论了8种模糊Kripke结构之间的关系。这些结论为设计应用中模型的合理选取提供了理论依据,也为解决模糊计算树逻辑的模型检测问题提供了一种新的方法。
| [1] Clarke E,Grumberg O,Peled D．Model Checking[M]．MITPress,1999 [2] Baier C,Katoen J P．Principles of Model Checking [M]．TheMIT Press,2007 [3] de Alfaro L,Faella M,Henzinger T A,et al．Model checking discounted temporal properties[J]．Theoretical Computer Science,2005,345(1):139-170 [4] Chechik M,Gurfnkel A,Devereux B,et al．Data structures forsymbolic multi-valued model-checking[J]．Formal Methods in Software Design,2006,29(3):295-344 [5] Kupferman O,Lusting Y．Latticed simulation relations andgames [J]．International Journal on the Foundations of Computer Science,2010,21(2):167-189 [6] 潘海玉.状态转化系统的格值量化验证方法研究[D].上海:华东师范大学,2012 [7] Li Y M,Pedrycz W．Fuzzy nite automata and fuzzy regular expressions with membership values in lattice ordered monoids [J].Fuzzy Sets and Systems,2005,6:68-92 [8] Li Z H,Li P,Li Y M．The relationships among several types of fuzzy automata[J].Information Sciences,2006,176:2208-2226 [9] Li Y M．Approximation and robustness of fuzzy finite automata[J].International Journal of Approximate Reasoning,2008,47(2):247-257 |
| No related articles found! |
|
||
首页